proposition: Lemma cardinal_doubleton x y: cardinal (doubleton x y) <=c \2c.
proof: Proof. case: (equal_or_not x y) => eq. rewrite eq; rewrite cardinal_set1; apply: cle_12. rewrite (cardinal_set2 eq); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)