proposition: Lemma card_quotient_subnorm A : #|A / H| = #|'N_A(H) : H|.
proof: Proof. by rewrite -(card_imset _ val_inj) val_quotient. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)