proposition: Lemma aleph_and_beth a: ordinalp a -> exists b, [/\ ordinalp b, beth b <=c \aleph a & \aleph a <c beth (osucc b)].
proof: Proof. move => oa; case: (normal_ofs_bounded (OS_aleph oa) (beth_normal)). by rewrite beth0 => /(oleNgt (aleph_pr5 oa)). move => [y [oy ha hb]]. have hc:=(CS_aleph oa). have hd:= (ocle3 (proj1 (beth_pr1 oy)) hc ha). have he:= (oclt3 hc (proj1 (beth_pr1 (OS_succ oy))) hb). by exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)