proposition: Lemma logn_morphim p G : logn p #|f @* G| <= logn p #|G|.
proof: Proof. by rewrite dvdn_leq_log ?dvdn_morphim. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)