proposition: Lemma rcosets_id G : rcosets G G = [set G : {set gT}].
proof: Proof. apply/esym/eqP; rewrite eqEcard sub1set [#|_|]indexgg cards1 andbT. by apply/rcosetsP; exists 1; rewrite ?mulg1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)