proposition: Lemma cardinal_ge3 E: \3c <=c cardinal E -> exists a b c, [/\ inc a E, inc b E, inc c E & [/\ a <> b, a <> c & b <> c]].
proof: Proof. rewrite /card_three - (card_card (CS_succ \2c)) (succ_of_nat NS2). move /eq_subset_cardP1 => [f [[ff injf] sf tf]]. exists (Vf f \0c); exists (Vf f \1c); exists (Vf f \2c). have zs: inc \0c (source f) by rewrite sf; apply /set3_P; in_TP4. have os: inc \1c (source f) by rewrite sf; apply /set3_P; in_TP4. have ts: inc \2c (source f) by rewrite sf; apply /set3_P; in_TP4. rewrite -tf;split; fprops; split=> h. by move: (injf _ _ zs os h); fprops. by move: (injf _ _ zs ts h); fprops. by move: (injf _ _ os ts h); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)