proposition: Lemma quotient_proper G K : H <| G -> H <| K -> (G / H \proper K / H) = (G \proper K).
proof: Proof. by move=> nHG nHK; rewrite -cosetpre_proper ?quotientGK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)