proposition: Lemma cofinality_sum2 a: ordinalp a -> singular_cardinal (\aleph(a +o omega0)).
proof: Proof. move => oa; move: (OS_sum2 oa OS_omega) => os. split; first by apply: CIS_aleph. rewrite (cofinality_sum1 oa) - {1} aleph0E => h. symmetry in h; move: (aleph_inj os OS0 h) => /(osum2_zero oa OS_omega) [_]. by move: omega_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)