proposition: Lemma beth_fixed_point x: ordinalp x -> beth x = x -> card_dominant x.
proof: Proof. move => ox bfx. have icx: infinite_c x by rewrite -bfx; apply: beth_pr1. have xnz:= (infinite_nz icx). have cx := proj1 icx. apply: card_dominant_pr1 => // m mx. have cm:= proj31_1 mx. move: (infinite_card_limit2 icx) => lx; move: (lx) =>[qa qb qc]. have [b pa pb]: exists2 b, m <=c beth b & b <o x. ex_middle bad. have pc:forall i, inc i (fun_image x beth) -> i <=c m. move => t /funI_P [i ix ->]. have oi:= Os_ordinal qa ix. case: (cleT_ee (CS_beth oi) cm) => // h; case: bad; exists i => //. by apply /oltP. have : union (fun_image x beth) <=c m. by apply: card_ub_sup. by rewrite - ((proj2 beth_normal) _ lx) bfx => /(cltNge mx). apply: (cle_ltT (cpow_Meqle card2_nz pa)). have ob:= proj31_1 pb. rewrite -(beth_succ ob) - bfx; apply: beth_M. by move: pb => /(oltP ox) hh; apply / (oltP ox);apply: qc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)