proposition: Lemma fconnect_findex_r (x y : T) : injective f -> fconnect f x y -> y != x -> findex f x y = (findex f x (finv f y)).+1.
proof: Proof. move=> inj_f con_xy yDx. by rewrite -[in RHS]findex_f 1?same_fconnect1_r ?f_finv // fconnect_findex . Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)