proposition: Lemma Exercise34a b: cardinalp b -> let A := Zo E (fun x => (cardinal (finv x)) <=c b) in let a := cardinal A in (\2c ^c a) <=c (csucc (a *c b)).
proof: Proof. move=> cb A a. move: (csucc_pr2 (setP_0i A)); rewrite card_setP - cpowcr =>->. set A' := \Po A -s1 emptyset; apply: cleSS. pose Ap x := Zo A' (fun z => f z = x). pose Af := Lg A Ap. have md: mutually_disjoint Af. rewrite /Af; apply: mutually_disjoint_prop; aw => i j t iA jA. by rewrite !LgV//;move => /Zo_P [_ <-] /Zo_P [_ <-]. have daf: domain Af = A by rewrite /Af; aw. have AE: sub A E by apply: Zo_S. move:(csum_pr4 md). have ->: unionb Af = A'. set_extens t;first by move/setUb_P =>[y]; rewrite daf /Af => yA; rewrite LgV// => /Zo_S. move => ta; move: (ta) => /Zo_P [/setP_P sY]. case: (emptyset_dichot t); first by move ->; case; fprops. move => net _; move: (choice (sub_trans sY AE) net) => ftt. apply/setUb_P; rewrite daf; move: (sY _ ftt) => h; ex_tac. by rewrite /Af LgV//; apply/Zo_P. move ->. rewrite /a cprod2cl cprodC -(csum_of_same) daf /Af. apply: csum_increasing; aw; trivial => y yA; rewrite !LgV//. move /Zo_P: yA => [_]. apply: cleT; apply: sub_smaller. move => t /Zo_P [/setC1_P [/setP_P ta _] ft]; apply/Zo_P; split => //. by apply/setP_P; apply: (sub_trans ta AE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)