proposition: Lemma cle2P E: \2c <=c (cardinal E) <-> exists a b, [/\ inc a E, inc b E & a <> b].
proof: Proof. split. rewrite - (card_card CS2) => /cardinal_le_aux1/(eq_subset_cardP \2c). move => /set_leP [x xE] => /card_eqP. rewrite (card_card CS2) => /esym. move/set_of_card_twoP => [a [b [anb xv]]]. exists a,b; split => //; apply: xE; rewrite xv; fprops. move => [x [y [xE yE nxy]]]. have sE: (sub (doubleton x y) E) by move=> t td; case/set2_P: td =>->; fprops. by rewrite - (cardinal_set2 nxy); apply: sub_smaller. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)