proposition: Lemma inaccessible_pr8_gch x: \2c <c x -> ([\/ (x = omega0), (exists2 n, ordinalp n & x = \aleph (osucc n)) | inaccessible x] <-> x = x ^<c x).
proof: Proof. move => x2. set p:= (exists2 n, ordinalp n & x = \aleph (osucc n)). have cx:=proj32_1 x2. have xnz : x <> \0c. move => xz; rewrite xz in x2; case: (clt0 x2). have xp:=(clt_ltT clt_02 x2). have aux: p -> x = x ^<c x. move => [n on xv]. rewrite {3} xv; move: (cpow_less_pr4 xp (CIS_aleph on)). rewrite (cnextE on); move => ->. have i1:=(CIS_aleph on). by rewrite xv - (cnextE on) (gch i1) - cpow_pow (csquare_inf). split. case =>//; first by move ->; symmetry; apply: cpow_less_pr5f. by apply: inaccessible_pr8. move => h. case: (finite_or_infinite cx) => fx. have xN: natp x by apply /NatP. move: (cpred_pr xN xnz)=> [ub uv]. move: (cpow_less_pr3 xp ub); rewrite -uv -h. move: (cltS ub); rewrite -uv => pa. have xp1: \1c <c cpred x. by apply/(cltSSP CS1 (proj31_1 pa)); rewrite - uv succ_one. move: (cpow_Meqlt xN ub xp1 (cle_ltT (proj1 xp1) pa)). by rewrite (cpowx1 cx); move => []. move: (ord_index_pr1 fx) => [om xv]; symmetry in xv. case: (ordinal_limA om) => ln. by constructor 1; rewrite - aleph0E - ln. move: ln => [n on nv]; constructor 2; exists n => //. by rewrite -nv. constructor 3;apply: inaccessible_weak_strong. split; last by exists (ord_index x). split => //; ex_middle cs. have cs1:=(cofinality_c_small (proj1 fx)). move: (cpow_less_pr2 x (conj cs1 cs)); rewrite -h => lt1. case: (cleNgt lt1(power_cofinality (proj1 x2))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)