proposition: Lemma Exercise5_9k4 n q k J (e:= nth_elt J) (e' := fun i => e i -c q *c i): natp q -> natp n -> k <=c n -> Ex59_Jprop q n k J -> [/\ forall i, i <c k -> natp (e' i), (forall i, i <c k -> e i = e' i +c q *c i), (forall i j, i <=c j -> j <c k -> e' i <=c e' j) & (forall j, j <c k -> e' j <=c q *c (n -c k)) ].
proof: Proof. move => qN nN lkn h. have kN:= NS_le_nat lkn nN. move:(Exercise5_9k2 kN h) =>[jpa _ _ jpd _]. move:(Exercise5_9k3 kN h) => [pa pb]. move: h => [cJ JN jp1 jp2]. have pc:(forall i, i <c k -> e i = e' i +c q *c i). by move => i ik; rewrite /e' csumC (cdiff_pr (pa _ ik)). have K: forall i, i <c k -> natp (e' i). by move => i /jpd/JN eN; apply:NS_diff. have pd': forall i, natp i -> csucc i <c k -> e' i <=c e' (csucc i). move => i iN sik. have sa:=(cltS iN); have sd := (NS_lt_nat sik kN); have se:= (clt_ltT sa sik). move: (jpd _ se) (jpd _ sik) => sb sc. move:(jp1 _ _ sb sc (jpa _ _ sa sik)). rewrite -/(e i) -/(e _)(pc _ se) (pc _ sik) - csumA - (cprod_nS _ iN). apply:(csum_le2r (NS_prod qN sd) (K _ se) (K _ sik)). have pd: forall i j, i <=c j -> j <c k -> e' i <=c e' j. move => i j lij ljk. move: (NS_lt_nat (cle_ltT lij ljk) kN) => iN. have kp:=(cle_ltT (cle0x (proj31_1 ljk)) ljk). move: (cpred_pr kN (nesym (proj2 kp))) => [sa sb]. move: ljk; rewrite sb; move/(cltSleP sa); move: j lij. apply:(Nat_induction3 iN sa); first by apply: (cleR (CS_diff _ _)). move => j jn jlk hr; apply:(cleT hr); apply: (pd' _ (NS_lt_nat jlk sa)). by rewrite sb; apply:cltSS. split => // j jk. have kp:=(cle_ltT (cle0x (proj31_1 jk)) jk). move: (cpred_pr kN (nesym (proj2 kp))) => [sa sb]. move:(cltS sa); rewrite - sb => lt1. move:(jk); rewrite sb; move/(cltSleP sa) => l2; apply:(cleT(pd _ _ l2 lt1)). move:(pb _ lt1); rewrite -/(e _) (pc _ lt1) -{1}(cdiff_pr lkn). rewrite - csumA - (cprod_nS _ sa) - sb cprodDr csumC. apply:(csum_le2l (NS_prod qN kN) (K _ lt1) (NS_prod qN (NS_diff k nN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)