proposition: Lemma LagrangeMl G H : (#|G| * #|H : G|)%N = #|G * H|.
proof: Proof. rewrite mulnC -(card_uniform_partition _ (rcosets_partition_mul H G)) //. by move=> _ /rcosetsP[x Hx ->]; rewrite card_rcoset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)