proposition: Lemma before_findex x z m : fconnect f x z -> m < findex f x z -> iter m f x != z.
proof: Proof. elim: m x z => [x z|n IHn x z xCz nz]; first by rewrite lt0n findex_eq0. have xDz : z != x by apply: contraTneq nz => ->; rewrite findex0. rewrite iterSr IHn -1?ltnS -?fconnect_findex //. by rewrite fconnect_eqVf eq_sym (negbTE xDz) in xCz. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)