proposition: Lemma beth_prop: [/\ normal_ofs beth, beth \0o = omega0 & (forall x, ordinalp x -> beth (osucc x) = \2c ^c (beth x)) ].
proof: Proof. apply: normal_ofs_existence. - move => x ox. move: (CS_pow \2c x) => cp. case: (oleT_el (proj1 cp) ox) => //. move /ocle1; rewrite (card_card cp) => /cleNgt; case. by move: (cantor (CS_cardinal x)); rewrite cpowcr. - move => x y /ocle1 /(cpow_Meqle card2_nz). rewrite cpowcr cpowcr; apply: ocle. - apply: OS_omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)