proposition: Lemma CR_prop7 n k (h := fun i => CR_partial_sum f i +q BQhalf (CR_inv3n i)): natp n -> natp k -> (h (n+c k) <=q h n).
proof: Proof. move => nN; move: k; apply:Nat_induction. rewrite (csum0r (CS_nat nN)); apply:qleR; apply: QSs. exact:(BQp_sBQ (CR_prop4 (NS_succ nN))). apply:(QS_half (CR_prop1 nN)). move => k kN hr. apply: qleT hr. rewrite (csum_nS _ kN) /h. have sN:= (NS_sum nN kN). move: (CR_prop6 sN) => hh. have ns3:= NS3. have nsp:= NS_pow ns3 sN. have Ha:= (CR_prop1 (NS_succ sN)). have Hb:= (QS_half Ha). have <-: (CR_inv3n (csucc (n +c k)) +q BQhalf (CR_inv3n (csucc (n +c k)))) = BQhalf (CR_inv3n (n +c k)). rewrite (CR_prop00 sN) -{1}(BQhalf_double Ha). by rewrite /BQhalf -(BQprodDl QSh2 (QSdouble Ha) Ha) BQ_double_plus. move/(BQsum_le2r (proj31 hh) (proj32 hh) Hb):hh. by rewrite (BQsumA (proj31 (CR_prop5 sN)) Ha Hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)