proposition: Lemma tcP_last x y : reflect (y \in h /\ exists n, iter' R n.+1 x y) (tc x y).
proof: Proof. case: tc_pathP_last=>H; constructor. case: H=>My [z][p][Rzy Pxp Lz]; split=>//; exists (size p); apply/iterS. by exists z; split=>//; apply/iter'_path; exists p. case=>My [n] /iterS [z][/iter'_path [p][Sp Pxp Lz] Rzy]. by apply: H; split=>//; exists z, p. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)