proposition: Lemma Exercise5_9i E q n: natp n -> natp q -> cardinal E = q *c n -> \0c <c q -> partition_w_fam (Lg (Nintc n) (Ex59_k_interval E q)) (partition_nq E q).
proof: Proof. move => nN qN cE qp. split; first fprops. hnf;aw => i j iN jN; rewrite !LgV//; mdi_tac nij => x /Zo_hi ha /Zo_hi hb. by case:nij; rewrite - ha -hb. set_extens t. by move/setUb_P => [y yI];rewrite Lgd in yI; rewrite LgV//; move/Zo_S. move => tp; apply /setUb_P; aw. have ct:=(partition_nq_pr2 (CS_nat nN) qN (nesym (proj2 qp)) cE tp). have lkn: inc (Ex59_nb_int q t) (Nintc n). by apply/(NintcP nN); rewrite - ct; apply/sub_smaller/Zo_S. by ex_tac; rewrite LgV//; apply:Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)