proposition: Lemma ord_sup_aleph x: limit_ordinal x -> \csup (range (Lg x \aleph)) = \aleph x.
proof: Proof. by move => lx; rewrite ((proj2 aleph_normal) _ lx) Lg_range. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)