proposition: Lemma cofinality_sum1 a: ordinalp a -> \cf (\aleph(a +o omega0)) = omega0.
proof: Proof. move => oa. rewrite (regular_initial_limit1 (osum_limit oa omega_limit)). rewrite (cofinality_sum oa olt_0omega). exact (proj2 regular_omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)