proposition: Lemma Exercise_6_20b a: \2c <c a -> (forall m, \0c <c m -> m <c a -> a ^c m = a) -> regular_cardinal a.
proof: Proof. move => a2 h. have ca:= proj32_1 a2. case: (finite_or_infinite ca). move /NatP => aN. move: (h _ clt_02 a2); rewrite cpowx2 => eq1. have aa: a <=c a by fprops. have anz: a <> \0c by move => eq2; rewrite eq2 in a2; case: (clt0 a2). move: (cprod_Mlelt aN aN aa a2 anz); rewrite eq1 => le1. case: (cltNge le1(cprod_M1le ca card2_nz)). move => ica; apply /regular_cardinalP; split; first by exact. ex_middle ne1. have sa: singular_cardinal a by split. have pa: (cpow_less_ec_prop a a \1c). split; first by apply: clt_fin_inf; fprops. move => b; rewrite (cpowx1 ca); move /cge1P => b1 ba. by rewrite (h _ b1 ba). move: (cantor ca); rewrite - (infinite_power1_b ica). move: (cpow_less_ec_pr3 pa (proj1 a2) sa) => [-> <-]. by rewrite (cpowx1 ca); move => []. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)