proposition: Lemma sub_cosetpre_quo C G : H <| G -> (coset H @*^-1 C \subset G) = (C \subset G / H).
proof: Proof. by move=> nHG; rewrite -cosetpreSK quotientGK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)