proposition: Lemma inaccessible_uncountable x: inaccessible_w x -> aleph0 <c x.
proof: Proof. move => sa. have bx:= (inaccessible_pr1 sa). rewrite bx /aleph0 - aleph0E; apply:aleph_lt_ltc;rewrite bx; apply: oclt. by move:(clt_leT clt_02 (infinite_ge2 (proj1 (proj1 sa)))); rewrite - bx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)