proposition: Lemma cardMg_TI G H : #|G| * #|H| <= #|G * H| -> G :&: H = 1.
proof: Proof. move=> leGH; apply: card_le1_trivg. rewrite -(@leq_pmul2l #|G * H|); first by rewrite -mul_cardG muln1. by apply: leq_trans leGH; rewrite muln_gt0 !cardG_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)