proposition: Lemma trivg_quotient : H / H = 1.
proof: Proof. by rewrite -[X in X / _]ker_coset /quotient morphim_ker. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)