proposition: Lemma coset_range_mul (B C : coset_of) : coset_range (B * C).
proof: Proof. case: B C => _ /= /rcosetsP[x Nx ->] [_ /= /rcosetsP[y Ny ->]]. by apply/rcosetsP; exists (x * y); rewrite !(groupM, rcoset_mul, nNH). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)