proposition: Lemma quotient_inj G1 G2 : H <| G1 -> H <| G2 -> G1 / H = G2 / H -> G1 :=: G2.
proof: Proof. by rewrite /normal -[in mem H]ker_coset; apply: morphim_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)