proposition: Lemma Exercise6_33o : [/\ inc alpha (cnext b), cardinal (Mi alpha) = c & forall m, inc m alpha -> cardinal (Mi m) <c c].
proof: Proof. rewrite /alpha/E6_33_alpha; set Z := Zo _ _. have oab: ordinalp (cnext b) by case : Exercise6_33a6. have nez: nonempty Z. move: Exercise6_33n => [m ml]; exists m; apply: Zo_i=> //. have oz: ordinal_set Z by move=> t => /Zo_P [/(Os_ordinal oab) tab _]. move: (least_ordinal0 oz nez) => [_ /Zo_P [lt pb] hz]. split => // m mc. have xab:= (ordinal_transitive oab lt mc). case/cle_eqVlt: (Exercise6_33m xab) => // cc. have /hz bad: inc m Z by apply: Zo_i. case: (ordinal_decent oab xab (proj33 bad _ mc)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)