proposition: Lemma card_dominant_pr3 x (y := next_dominant x) : cardinalp x -> \2c ^c y = y ^c omega0.
proof: Proof. move => cx; move: (next_dominant_pr cx); rewrite -/y. move=> [[iy yp] _]. move: (iy) => [cy _ _]. have oy: omega0 <=c y by apply /infinite_c_P2. have co:= CS_omega. apply: cleA; last first. rewrite -(infinite_power1_b iy). apply:cpow_Mlele; fprops; by apply: infinite_nz. move: (induction_defined_pr (cpow \2c) x) => /=. set f := (induction_defined (cpow \2c) x). move => [qa [rb qb2] qc qd]. have bv: y = \osup (target f) by done. have ra: fgraph (Lg omega0 (Vf f)) by fprops. have bv1: y = \osup (range (Lg omega0 (Vf f))). rewrite bv; apply: f_equal; set_extens t. move /qb2=> [u usf ->]; apply /(range_gP ra); aw. rewrite qa in usf;exists u => //; rewrite LgV//. move /(range_gP ra); aw; move => [u usf ]; rewrite LgV//; move => ->; Wtac; ue. have rd0: forall u, natp u -> cardinalp (Vf f u). apply: Nat_induction; first ue. move=> n nN _; rewrite (qd _ nN) /cpow; fprops. have rd: cardinal_fam (Lg omega0 (Vf f)) by hnf; aw => t tw;rewrite LgV; fprops. have bv2: y = csum (Lg omega0 (Vf f)). by rewrite csum_of_small_b4 // - bv1 // Lgd (card_card co). rewrite {1} bv2 cpow_sum Lgd - cprod_of_same. have cs1: (cardinal_set (target f)). by move => t /qb2 [u usf ->];apply: rd0; rewrite /natp - qa. apply: cprod_increasing; aw; trivial => t tN; rewrite !LgV//. by rewrite -(qd _ tN); apply: (card_sup_ub cs1); Wtac;rewrite qa; apply:NS_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)