proposition: Lemma Exercise6_33m x: inc x (cnext b) -> cardinal (Mi x) <=c c.
proof: Proof. move => xs. have s1: sub (Mi x) M by move =>t ti; rewrite Exercise6_33l; apply /setUf_P; ex_tac. by move: (sub_smaller s1); rewrite Exercise6_33f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)