proposition: Lemma cardinal_set2 x x': x <> x' -> cardinal (doubleton x x') = \2c.
proof: Proof. move => /set2_equipotent_aux /proj31;set g := Lf _ _ _ => bg. by rewrite -(card_card CS2);apply /card_eqP; exists g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)