proposition: Lemma iter_path x y : iter R x y <-> exists2 p, path R x p & y = last x p.
proof: Proof. split; first by case=>n /iter'_path [p][Sp Pxp Ly]; exists p. by case=>p Pxp Ly; exists (size p); apply/iter'_path; exists p. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)