proposition: Lemma card_gt2P A : reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x]) (2 < #|A|).
proof: Proof. apply: (iffP card_geqP) => [[s] []|[x] [y] [z] [[xD yD zD] [xDy xDz yDz]]]. case: s => [|x [|y [|z []]]]//=; rewrite !inE !andbT negb_or -andbA. case/and3P => xDy xDz yDz _ subA. by exists x, y, z; rewrite xDy yDz eq_sym xDz !subA ?inE ?eqxx ?orbT. exists [:: x; y; z]; rewrite /= !inE negb_or xDy xDz eq_sym yDz; split=> // u. by rewrite !inE => /or3P [] /eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)