proposition: Lemma Exercise6_33s: exists N z, E6_33_N_prop N z.
proof: Proof. move: Exercise6_33r; set T := functions _ _; move => Ha. pose f x := Zo N0 (fun n => yr n = x). have fi i j: inc i T -> inc j T -> i = j \/ disjoint (f i) (f j). move => iN jN. mdi_tac u => x /Zo_hi xi /Zo_hi xj. by case: u; rewrite - xi xj. move: (@csum_pr4_bis T f fi). have ->: (unionf T f) = N0. set_extens t. by move => /setUf_P [i iN /Zo_P[qa qb]]. move => tn; apply /setUf_P; exists (yr t); last by apply: Zo_i. by move: (proj32 (Ha _ tn)). case: (all_exists_dichot1 (fun i=> cardinal (f i) <=c a ^c b) T) => H. move: (cltNge Exercise6_33b) => bad. pose fa := Lg T (fun x => (cardinal (f x))). pose fb := Lg T (fun x => a ^c b). have dd: domain fa = domain fb by rewrite /fa /fb; aw. have cp: (forall x, inc x (domain fa) -> Vg fa x <=c Vg fb x). by rewrite /fa/fb; aw => x xd; bw => //; apply: H. move: Exercise6_33q =>[_ _ n_ _ ->] => eq1. move: (csum_increasing dd cp). rewrite /fa /fb -/(csumb _ _) -/(csumb _ _) - eq1 csum_of_same. rewrite - cprod2cr /T - /(cpow _ _) - (cpowcr _ alpha). rewrite - (cpowcl (unionf _ _)). case: (equal_or_not (cardinal (unionf alpha Mi)) \0c) => Ms. rewrite Ms; case: (equal_or_not (cardinal alpha) \0c) => As. by rewrite As cpow00 cprod1r; fprops => w; case: bad. rewrite cpow0x // cprod0r => /cle0 cz. by case: (infinite_nz (Exercise6_33c)). move: (proj2((proj44 (Exercise6_33a6)) _ (proj31 (Exercise6_33o)))) => lab. move: Exercise6_33p => /Exercise6_33aP qa. move: (cpow_Mlele Ms qa lab); rewrite - cpow_pow Exercise6_33a1. set w := _ ^c _ => hc hd. by move: (cleT hd (cprod_inf1 hc Exercise6_33a)) => cs; case: bad. case: H => z zT lt1 _. set N := f z. have sN0: sub N N0 by apply: Zo_S. move: (sub_smaller sN0). move: Exercise6_33q =>[_ _ _ _ cn0]; rewrite cn0. case/ cle_eqVlt; [move => cn | by move/(cnext_pr4 (CS_pow a b)) ]. by exists N, z; split => // i /Zo_P[qa qb]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)