proposition: Lemma prime_meetG G H : prime #|G| -> G :&: H != 1 -> G \subset H.
proof: Proof. by move=> prG; apply: contraR; move/prime_TIg->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)