proposition: Lemma next_dominant_pr x (y:= next_dominant x): cardinalp x -> [/\ card_dominant y , x <c y & (forall z, card_dominant z -> x <c z -> y <=c z)].
proof: Proof. move => cx; rewrite /y /next_dominant; clear y. rewrite /the_least_fixedpoint_ge. move: (induction_defined_pr (cpow \2c) x). set f := induction_defined _ _; move=> [sf [ff sjf f0 fnz]]. have cs1: forall n, natp n -> cardinalp (Vf f n). apply: Nat_induction; first ue. move=> n nN _; rewrite (fnz _ nN) /cpow; fprops. have cs: cardinal_set (target f). by move => t /sjf; rewrite sf; move=> [u ub ->]; apply: cs1. set y:= \osup (target f). have ltxy: x <c y. apply (clt_leT (cantor cx)); apply: (card_sup_ub cs). rewrite - f0 - (fnz _ NS0); Wtac; rewrite sf; apply:NS_succ; fprops. split => //. apply: card_dominant_pr1 => //; first by apply: (CS_sup cs). move => yz; rewrite yz in ltxy; case: (clt0 ltxy). move=> m my. have [n pd pe]: exists2 n, inc n (target f) & m <=c n. ex_middle bad. have cm:= proj31_1 my. have pd: forall t, (inc t (target f) -> t <=c m). move=> t ti. case: (cleT_ee (cs _ ti) cm) => // b1; case: bad;ex_tac. case: (cltNge my (card_ub_sup cm pd)). move: (sjf _ pd) => [u us uv]. have le1: \2c ^c m <=c \2c ^c n by apply: cpow_Meqle; fprops. have le2: \2c ^c n <c \2c ^c ( \2c ^c n). apply: cantor; rewrite /cpow; fprops. apply: (cle_ltT le1); apply: (clt_leT le2). apply (card_sup_ub cs); aw; rewrite sf in us. rewrite uv - (fnz _ us) - (fnz _ (NS_succ us)); Wtac; rewrite sf. rewrite -/(natp _);fprops. move=> z [iz dz] xz; apply card_ub_sup; first by exact (proj1 iz). move => a /sjf; rewrite sf; move=> [n nB ->]. suff : Vf f n <c z by move=> []. move: n nB; apply: Nat_induction; first by ue. move=> n nB le1; rewrite (fnz _ nB); apply: dz => //. apply: clt_fin_inf => //; rewrite /NatP; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)