proposition: Lemma aleph_sum_pr1 x: ordinalp x -> inc x omega0 \/ exists2 y, ordinalp y & inc x (aleph_succ_comp y).
proof: Proof. move=> ox. case: (normal_ofs_bounded ox aleph_normal) => h. by left; move: h; rewrite -aleph0E; move /oltP0; move=> [_ _]. by move: h => [y [pa pb pc]]; right; exists y => //; apply /(aleph_succ_P1 pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)