proposition: Lemma coprime_TIg G H : coprime #|G| #|H| -> G :&: H = 1.
proof: Proof. move=> coGH; apply/eqP; rewrite trivg_card1 -dvdn1 -{}(eqnP coGH). by rewrite dvdn_gcd /= {2}setIC !cardSg ?subsetIl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)