proposition: Lemma ord_sup_aleph_sum x: ordinalp x -> \csup (range (Lg omega0 (fun z=> \aleph (x +o z)))) = \aleph (x +o omega0).
proof: Proof. move => ox. move: (normal_ofs_compose aleph_normal (osum_normal ox)) => [_ xb]. by move: (xb _ omega_limit) => /= ->; rewrite Lg_range. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)