proposition: Lemma inaccessible_pr4 x: \2c <c x -> (forall f, cprod_of_small f x -> cprod f <c x) -> (x = omega0 \/ (exists2 n, limit_ordinal n & x = \aleph n)).
proof: Proof. move=> x2 h. move: (inaccessible_pr3 x2 h) => [pa pb]. move: (ord_index_pr1 pa) => [on xv]; rewrite -xv. case: (ordinal_limA on) => ln; last by right; exists (ord_index x). left; rewrite ln; apply: aleph0E. move: ln => [m om mv]. move: (cnext_pr1 (CS_aleph om)). rewrite (cnextE om) - mv xv; move => [pc pd pe]. move: (pb _ _ pd pd); rewrite (infinite_power1_b (CIS_aleph om)). rewrite - {1} xv mv => /(aleph_pr10a om) => l2. case: (cleNgt l2 (cantor (proj31_1 pd))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)