proposition: Lemma tc_pathP_last x y : reflect (y \in h /\ exists z p, [/\ R z y, path R x p & z = last x p]) (tc x y).
proof: Proof. case: tc_pathP=>H; constructor. - case: H=>Mx [z][p][Rxz Pzp Ly]; split. - by rewrite {1}Ly -(path_closed Pzp) -(Rclosed Rxz). case: (lastP p) Pzp Ly=>[|q w]; first by move=>_ ->; exists x, [::]. rewrite rcons_path last_rcons=>/andP [Pzw Rwq ->{y}]. by exists (last z q), (z::q); rewrite /= Rxz. case=>My [z][p][Rzy Pxp Lz]; apply: H; split. - by rewrite (path_closed Pxp) -Lz (Rclosed Rzy). case: p Pxp Lz=>[|w q] /=; first by move=>_ <-; exists y, [::]. case/andP=>Rxw Pwq E; exists w, (rcons q y). by rewrite rcons_path last_rcons -E Pwq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)