proposition: Lemma rcosets_partition_mul G H : partition (rcosets H G) (H * G).
proof: Proof. set HG := H * G; have sGHG: {subset G <= HG} by apply/subsetP/mulG_subr. have defHx x: x \in HG -> [set y in HG | rcoset H x == rcoset H y] = H :* x. move=> HGx; apply/setP=> y; rewrite inE !rcosetE (sameP eqP rcoset_eqP). by rewrite rcoset_sym; apply/andb_idl/subsetP; rewrite mulGS sub1set. have:= preim_partitionP (rcoset H) HG; congr (partition _ _); apply/setP=> Hx. apply/imsetP/idP=> [[x HGx ->] | ]; first by rewrite defHx // mem_rcosets. by case/rcosetsP=> x /sGHG-HGx ->; exists x; rewrite ?defHx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)