proposition: Lemma orbit_rot1 (inj_f : injective f) x : orbit f (f x) = rot 1 (orbit f x).
proof: Proof. have [fx_x|fxNx] := eqVneq (f x) x; first by rewrite fx_x orbit_fix. suff S : index (f x) (orbit f x) = 1. rewrite (orbitE (cycle_orbit inj_f x)) ?S //. by rewrite -fconnect_orbit -same_fconnect1_r. rewrite /orbit -orderSpred /= eq_sym (negPf fxNx). by case: (_.-1) => //= n; rewrite eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)