proposition: Lemma cardinal_setC3_rev: exists a b, a =c b /\ ~ (a -s b) =c (b -s a).
proof: Proof. move: omega0_pr => [qa qb _]. exists omega0, (osucc omega0); split; first by apply/card_eqP. have -> :omega0 -s osucc omega0 = emptyset. by apply/set0_P => t /setC_P [to]; case; apply: setU1_r. have ->: (osucc omega0 -s omega0) = singleton omega0. set_extens t; first by case/setC_P;case /setU2_P. move => /set1_P ->; apply/setC_P; split; first fprops. apply: (ordinal_irreflexive qa). rewrite cardinal_set0 cardinal_set1; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)