proposition: Lemma Exercise5_9l4 n q p k J x y: natp n -> natp q -> \0c <c q -> Ex59_Cprop n q J k p -> inc x p -> inc y x -> y <c q *c n.
proof: Proof. move => nN qN qp [/Zo_P [/partitionsP [[ha _] _]]] _ _ _ xp yp. have nqN:=NS_prod qN nN. have /setC_P [/(NintP nqN) //]: inc y (Ex59_compl n q J). by rewrite - ha; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)