proposition: Lemma Exercise6_33n: exists2 m, inc m (cnext b) & (cardinal (Mi m)) = c.
proof: Proof. ex_middle pa; case: (cltNge (Exercise6_33b)). move /Exercise6_33aP: (proj42 Exercise6_33a6) => hc. have h: (forall i, inc i (cnext b) -> cardinal (Mi i) <=c a ^c b). move => i xab. move:(Exercise6_33m xab); case/Exercise6_33a5 => // ee; case: pa; ex_tac. move:(csum_pr1_bnd h); rewrite - Exercise6_33l Exercise6_33f => q. rewrite - (csquare_inf Exercise6_33a). by apply: (cleT q); apply: cprod_Meqle. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)