proposition: Lemma inaccessible_pr1 x: inaccessible_w x -> x = \aleph x.
proof: Proof. move=> [/regular_cardinalP [xx re] [n ln xv]]. have on: ordinalp n by move: ln => []. move: (osi_gex aleph_lt_lto on) => le1. case: (equal_or_not n (\aleph n)) => eq; first by rewrite xv - {2} eq. move: (regular_initial_limit3 ln (conj le1 eq))=> [_]. by rewrite -xv re. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)