proposition: Lemma inaccessible_pr8 x: inaccessible x -> x = x ^<c x.
proof: Proof. move => h; move: (h) => [[[pa1 pa2] pb] pc]; move: (proj1 pa1) => cx. apply: cleA. by move: (cpow_less_pr2 x (infinite_gt1 pa1)); rewrite (cpowx1 cx). apply: card_ub_sup => // t /funI_P [z z1 ->]. move: z1 => /(cardinals_ltP cx) => z1. case: (equal_or_not z \0c) => xnz. rewrite xnz cpowx0; apply (proj1 (infinite_gt1 pa1)). move: (inaccessible_pr7 h xnz z1) => ->. apply: (cleR (proj32_1 z1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)