proposition: Lemma quotient_neq1 A : H <| A -> (A / H != 1) = (H \proper A).
proof: Proof. case/andP=> sHA nHA; rewrite /proper sHA -trivg_quotient eqEsubset andbC. by rewrite quotientS //= quotientSGK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)