proposition: Lemma TI_cardMg G H : G :&: H = 1 -> #|G * H| = (#|G| * #|H|)%N.
proof: Proof. by move=> tiGH; rewrite mul_cardG tiGH cards1 muln1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)