proposition: Lemma beth_pr1 x: ordinalp x -> infinite_c (beth x).
proof: Proof. move => ox; case: (ozero_dichot ox). move => ->; rewrite beth0; apply CIS_omega. by move /beth_M; rewrite beth0; move => [/infinite_c_P2 le1 _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)