proposition: Lemma Exercise5_9k6 n q k f (J := fun_image k (fun i => Vf f i +c q *c i)) (T := functions_incr_nat k (csucc (q *c (n -c k)))): natp q -> natp n -> k <=c n -> \0c <c q -> inc f T -> [/\ Ex59_Jprop q n k J, forall i, i <c k -> (nth_elt J i) = Vf f i +c q *c i & forall i, i <c k -> (nth_elt J i) -c q *c i = Vf f i].
proof: Proof. move => qN nN lkn qp. have kN := NS_le_nat lkn nN. have tN:=(NS_prod qN (NS_diff k nN)). move/(increasing_nat_prop kN (NS_succ tN)) => [/functionsP [ff sf tf] ficf]. have tfn i: inc i k -> natp (Vf f i). rewrite - sf => zz. by move:(Vf_target ff zz); rewrite tf; move/ (NS_inc_nat (NS_succ tN)). have JN: sub J Nat. move => i /funI_P [z zz ->]. exact: (NS_sum (tfn _ zz) (NS_prod qN (NS_inc_nat kN zz))). have inc2 i j: inc i k -> inc j k -> i <c j -> Vf f i +c q *c i <c Vf f j +c q *c j. move => iI jI lij. move/(NltP kN): (jI) => ljk. have li2 :=(ficf i j (proj1 lij) ljk). apply:(csum_Mlelt (tfn _ jI) li2). apply:(cprod_Meqlt qN (NS_lt_nat ljk kN) lij (nesym (proj2 qp))). have inc3 i j: inc i k -> inc j k -> Vf f i +c q *c i <c Vf f j +c q *c j -> i<c j. move => iI jI h. case:(NleT_ell (NS_inc_nat kN iI) (NS_inc_nat kN jI)) => // lij. - by case: (proj2 h); rewrite lij. - case: (cltNge (inc2 _ _ jI iI lij) (proj1 h)). have cj:cardinal J = k. rewrite -(card_card (CS_nat kN)); apply:cardinal_fun_image => i j iI jI eq1. case:(NleT_ell (NS_inc_nat kN iI) (NS_inc_nat kN jI)) => // lij. by case:(proj2 (inc2 _ _ iI jI lij)). by case:(proj2 (inc2 _ _ jI iI lij)). have si2 u v: inc u J -> inc v J -> u <c v -> u +c q <=c v. move => /funI_P [i iI ->] /funI_P [j jI ->] h. move:(inc3 _ _ iI jI h) (NS_inc_nat kN iI) => lij iN. move/(NltP kN): jI => ljk. rewrite - csumA;apply:(csum_Mlele (ficf _ _ (proj1 lij) ljk)). by rewrite - (cprod_nS _ iN); apply: cprod_Meqle;apply/(cleSltP iN). have si4 j: inc j J -> j +c q <=c q *c n. move => /funI_P [i iI ->]; rewrite - csumA. have iN:= (NS_inc_nat kN iI). move/(NltP kN): (iI) => lik. have le1: (q *c i +c q) <=c q *c k. by rewrite - (cprod_nS _ iN); apply: cprod_Meqle;apply/(cleSltP iN). move: iI;rewrite - sf => zz. move:(Vf_target ff zz); rewrite tf => /(NleP tN) le2. by move:(csum_Mlele le2 le1); rewrite - cprodDr (csumC _ k) (cdiff_pr lkn). have enuu:forall i, i <c k -> nth_elt J i = Vf f i +c q *c i. have ha1:forall i, i <c k -> natp (Vf f i +c q *c i). move => i /(NltP kN) ik; apply:JN; apply/funI_P; ex_tac. have ha2 i j:i <c j -> j <c k -> Vf f i +c q *c i <c Vf f j +c q *c j. move => lij h1; apply:(inc2)(lij); apply/(NltP kN) => //. exact:(clt_ltT lij h1). exact:(nth_elt_exten kN ha1 ha2). have Jp: Ex59_Jprop q n k J by []. move: (Exercise5_9k4 qN nN lkn Jp) => [sa sb sc sd]. split => // i ik; rewrite (enuu _ ik); apply:cdiff_pr1. by apply:tfn; apply/(NltP kN). exact: (NS_prod qN (NS_lt_nat ik kN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)