proposition: Lemma cardinal_tripleton x y z: x <> y -> x <> z -> y <> z -> cardinal (tripleton x y z) = \3c.
proof: Proof. move => xy xz yz. rewrite /tripleton csucc_pr ? cardinal_set2 //. by case /set2_P; apply: nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)