proposition: Lemma order_f (inj_f : injective f) x: order f (f x) = order f x.
proof: Proof. by apply/(orbitPcycle 1 2); rewrite /= inE -same_fconnect1. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)