proposition: Lemma findex_f (x y : T) : injective f -> fconnect f x y -> findex f (f x) (f y) = findex f x y.
proof: Proof. move=> inj_f conn_xy; apply/eqP; rewrite eqn_leq; apply/andP;split. by apply: findex_bound; rewrite -iterSr iterS iter_findex. apply: findex_bound; rewrite -[iter _ _ _](finv_f inj_f) -iterS iterSr. by rewrite iter_findex ?finv_f // -same_fconnect1 -?same_fconnect1_r. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)