proposition: Lemma TIp1ElemP p A X Y : X \in 'E_p^1(A) -> Y \in 'E_p^1(A) -> reflect (X :&: Y = 1) (X :!=: Y).
proof: Proof. move=> EpX EpY; have p_pr := pnElem_prime EpX. have [oX oY] := (card_p1Elem EpX, card_p1Elem EpY). have [<-|] := eqVneq. by right=> X1; rewrite -oX -(setIid X) X1 cards1 in p_pr. by rewrite eqEcard oX oY leqnn andbT; left; rewrite prime_TIg ?oX. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)