proposition: Lemma rcosets_partition G H : H \subset G -> partition (rcosets H G) G.
proof: Proof. by move=> sHG; have:= rcosets_partition_mul G H; rewrite mulSGid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)