proposition: Lemma quotient1_isom : isom A (A / 1) (coset 1).
proof: Proof. by apply: sub_isom coset1_injm; rewrite ?norms1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)