proposition: Lemma prime_TIg G H : prime #|G| -> ~~ (G \subset H) -> G :&: H = 1.
proof: Proof. case/primeP=> _ /(_ _ (cardSg (subsetIl G H))). rewrite (sameP setIidPl eqP) eqEcard subsetIl => /pred2P[/card1_trivg|] //= ->. by case/negP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)