proposition: Lemma coset_range_inv (B : coset_of) : coset_range B^-1.
proof: Proof. case: B => _ /= /rcosetsP[x Nx ->]; rewrite norm_rlcoset ?nNH // invg_lcoset. by apply/rcosetsP; exists x^-1; rewrite ?groupV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)