proposition: Lemma Exercise5_9k1 n q p k (E:= Nint (q *c n)): natp n -> natp q -> \0c <c q -> inc p (Ex59_k_interval E q k) -> Ex59_Jprop q n k (Ex59_splitA q p).
proof: Proof. move => nN qN qp pI. move:(pI) => /Zo_S /Zo_P [/partitionsP [[pp cp] _ ] _]. have ce:cardinal E = q *c n by apply:card_Nint; fprops. set J := (Ex59_splitA q p). have JN: sub J Nat by move => t tJ; exact:proj1(Exercise5_9j3 qN qp tJ). have cJ:= (proj1 (Exercise5_9j5 nN qN qp ce pI)). split => //. move => i j /(Exercise5_9j3 qN qp) [iN ip] /(Exercise5_9j3 qN qp) [jN jp]. move => [lij nij]. case: (cleT_el (CS_sum2 i q) (CS_nat jN)) => // la. move/(Ex59_interval_prop iN qN qp) : (conj lij la) => jii. move: (csum_Meqlt jN qp); rewrite (csum0r (CS_nat jN)) => ljn. have jij: inc j (Nintcc j (j +c (q -c \1c))). apply/(Ex59_interval_prop jN qN qp); split; fprops. case: (cp _ _ ip jp) => di; last by empty_tac1 j. case: nij; exact (Nintcc_exten_spec qN iN di). move => i /(Exercise5_9j3 qN qp) [iN ip]. have la: i <=c (i +c (q -c \1c)) by apply:csum_M0le; fprops. have ea:=(Ex59_intp qN qp iN). have bi := NS_sum iN (NS_diff \1c qN). set j := (i +c (q -c \1c)). have jI: inc j (Nintcc i (i +c (q -c \1c))). apply/(Ex59_interval_prop iN qN qp); split; first exact. rewrite ea; apply /(cltSleP bi); fprops. have /(NintP (NS_prod qN nN)) : inc j E by rewrite - pp;union_tac. by move /(cleSltP bi); rewrite - ea. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)