proposition: Lemma card_morphpre L : L \subset f @* D -> #|f @*^-1 L| = (#|'ker f| * #|L|)%N.
proof: Proof. move/morphpreK=> {2} <-; rewrite card_morphim morphpreIdom. by rewrite Lagrange // morphpreS ?sub1G. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)