proposition: Lemma rtc_pathP_last x y : reflect (y \in h /\ exists2 p, path R x p & y = last x p) (rtc x y).
proof: Proof. case: rtc_pathP=>[[pfx]|] H; constructor. - by split=>//; case: H pfx=>p /path_closed ->->. by case=>pfy X; apply: H; split=>//; case: X pfy=>p /path_closed ->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)