Variable A : Set.

Variables x1 x2 x3 x4 x5 : A.

Variable R : A -> A -> Prop.

Variable Rtrans : forall x y z, R x y -> R y z -> R x z.

Ltac trans := 
   match goal with 
     | id : R ?x ?y |- R ?x ?y => exact id
     | id : R ?x ?z |- R ?x ?y => apply Rtrans with (1:=id)
     | id : R ?z ?y |- R ?x ?y => apply Rtrans with (2:=id)
end.

Lemma test : R x1 x2 -> R x2 x4 -> R x4 x5 -> R x1 x5.
intros.
repeat trans.
Save.