proposition: Lemma aleph_succ_pr2 x: ordinalp x -> cardinal (aleph_succ_comp x) = \aleph (osucc x).
proof: Proof. move => ox. move:(CIS_aleph (OS_succ ox)) (aleph_lt_lto (oltS ox)) => sa sb. exact (proj2 (cardinal_indecomposable1 sa sb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)