proposition: Lemma coset_one_proof : coset_range H.
proof: Proof. by apply/rcosetsP; exists (1 : gT); rewrite (group1, mulg1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)