proposition: Lemma eq_findex (T : finType) (f g : T -> T) : f =1 g -> findex f =2 findex g.
proof: Proof. move=> fg x y; rewrite /findex /index /orbit /order (eq_traject fg). congr (_ _ (traject _ _ _)); exact/eq_card/eq_fconnect. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)