proposition: Lemma tc_trans : transitive tc.
proof: Proof. rewrite /tc=>x y z /andP [Dy /hasP [y' Dy' /andP [Ry Ry'x]]]. case/andP=>Dx /hasP [x' Dx' /andP [Rx Rx'z]]. rewrite Dy; apply/hasP; exists y'=>//; rewrite Ry. by apply: rtc_trans (rtc_trans Ry'x (rtc1 _ _ _)) Rx'z. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)