proposition: Lemma orbit_fix x : f x = x -> orbit f x = [:: x].
proof: Proof. move => fx; rewrite /orbit (_ : order f x = 1) //. by apply/eqP; rewrite eqn_leq order_gt0 andbT; apply: order_le_fix. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)