proposition: Lemma order_injm x : x \in D -> #[f x] = #[x].
proof: Proof. by move=> Dx; rewrite orderE -morphim_cycle // card_injm ?cycle_subG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)