proposition: Lemma cardinal_omega2: cardinal omega0 = cardinal (omega0 +o omega0).
proof: Proof. move: OS_omega => o_o. rewrite osum_cardinal // csum_inf1 // (card_card CS_omega). exact:CIS_omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)