proposition: Lemma Exercise5_9k3 n q k J (e := nth_elt J): natp k -> Ex59_Jprop q n k J -> (forall i, i<c k -> q *c i <=c e i) /\ (forall j, j <c k -> e j +c q <=c q *c n).
proof: Proof. move => kN JP; move:(Exercise5_9k2 kN JP) =>[jpa _ _ jpd _]. move: JP => [cJ JN jp1 jp2]. split; last by move => i /jpd /jp2. move => i ik; move: (NS_lt_nat ik kN) => iN; move: i iN ik. apply: Nat_induction. move => kp;rewrite cprod0r; apply:(cle0n (JN _ (jpd _ kp))). move => i iN Hi lik. have lisi:= (cltS iN). have lt2:= (clt_ltT lisi lik). apply:cleT (jp1 _ _ (jpd _ lt2) (jpd _ lik) (jpa _ _ lisi lik)). rewrite (cprod_nS _ iN); apply:csum_Mleeq ; exact: (Hi lt2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)