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