proposition: Lemma coprime_cardMg G H : coprime #|G| #|H| -> #|G * H| = (#|G| * #|H|)%N.
proof: Proof. by move=> coGH; rewrite TI_cardMg ?coprime_TIg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)