proposition: Lemma set_of_card_twoP x: cardinal x = \2c <-> doubletonp x.
proof: Proof. split; last by move => [a [b [nab ->]]]; apply: cardinal_set2. move/esym;rewrite -(card_card CS2); move /card_eqP. move=> [f [[[ff injf] [_ sf]] srf <-]]. rewrite srf in injf sf. have es: inc \0c \2c by fprops. have ses: inc \1c \2c by fprops. exists (Vf f \0c), (Vf f \1c); split. by move=> aux; move: (injf _ _ es ses aux); fprops. set_extens t. move /sf => [z zsf ->]; case/set2_P:zsf => ->; fprops. case /set2_P => ->; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)