proposition: Lemma beth_inaccessible a k : inaccessible k -> a <o k -> beth a <c k.
proof: Proof. move => [ina inb] sb. have oa:= (proj31_1 sb). move: sb. case: (least_ordinal6 (fun a => a <o k -> beth a <c k) oa) => //. set y:= least_ordinal _ _; move => [oy pb]; case => lyk. case: (ordinal_limA oy). - by move ->; rewrite beth0; move: (inaccessible_uncountable ina). - move => [x ox yv]. have xy: inc x y by rewrite yv; fprops. have lxk: x <o k by apply:olt_ltT lyk; move /(oltP oy): xy. rewrite yv (beth_succ ox); exact: (inb _ (pb _ xy lxk)). - move => ly; rewrite (proj2 beth_normal _ ly). have ck:= (proj1 (proj1(proj1 ina))). move/(ocle2P ck (proj31_1 lyk)): (lyk) => cyk. have ha:=(cle_ltT (fun_image_smaller y beth) cyk). apply: (regular_sup (proj1 ina) ha) => i /funI_P [z zy ->]. have lzy: z <o y by apply /(oltP (proj31 ly)). exact: (pb _ zy (olt_ltT lzy lyk)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)