proposition: Lemma cosetpreM C D : coset H @*^-1 (C * D) = coset H @*^-1 C * coset H @*^-1 D.
proof: Proof. by rewrite morphpreMl ?sub_im_coset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)