proposition: Lemma singular_non_collectivizing: not (exists E, forall x, singular_cardinal x -> inc x E).
proof: Proof. move=> [E ep]. set F := Zo E singular_cardinal. have ce: cardinal_set F by move => t /Zo_P [_ [[pa _] _]]. move: regular_initial_limit4 => h. have ef: inc (\aleph omega0) F by apply: Zo_i => //; apply: ep. move: (cle_inf_inf (CIS_aleph OS_omega) (card_sup_ub ce ef)) => ins. move: (ord_index_pr1 ins) =>[]; set n := ord_index _ => on yv. have h1:= (cofinality_sum2 on). have xf: inc (\aleph (n +o omega0)) F by apply: Zo_i => //; apply: ep. move: (card_sup_ub ce xf); rewrite -yv => h2. move: (aleph_lec_le (OS_sum2 on OS_omega) on h2). by move: (osum_Meqlt olt_0omega on); rewrite (osum0r on) => pa /(oltNge pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)