proposition: Lemma quotientS1 G : G \subset H -> G / H = 1.
proof: Proof. by move=> sGH; apply/trivgP; rewrite -trivg_quotient quotientS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)