proposition: Lemma CR_prop8 n k: natp n -> natp k -> CR_partial_sum f k <=q CR_partial_sum f n +q (CR_inv3n n).
proof: Proof. move => nN kN. case: (NleT_ee kN nN) => lkn. have Ha: CR_partial_sum f n <=q CR_partial_sum f n +q CR_inv3n n. apply:(BQsum_Mp (proj31 (CR_prop5 nN)) (BQps_sBQp (CR_prop0 nN))). apply:(qleT _ Ha). rewrite -(cdiff_pr lkn); move:(NS_diff k nN); move:(_ -c _). apply: Nat_induction. by rewrite (csum0r (CS_nat kN)); exact:(qleR (proj31 (CR_prop5 kN))) => xQ. move => m mN Hr; apply: (qleT Hr);rewrite (csum_nS _ mN). exact:(CR_prop5 (NS_sum kN mN)). move:(cdiff_pr lkn)(NS_diff n kN); set m := (_ -c _) => kv mN. move: (CR_prop7 nN mN); rewrite kv => hb. have ha: (CR_partial_sum f k) <=q CR_partial_sum f k +q BQhalf (CR_inv3n k). apply:(BQsum_Mp (proj31 (CR_prop5 kN))). exact: (BQps_sBQp (BQhalf_pos (CR_prop0 kN))). apply: (qleT (qleT ha hb)). have qa:= (CR_prop0 nN); have qb := (BQps_sBQ qa). apply /(BQsum_le2l (QS_half qb) qb (proj31 (CR_prop5 nN))). exact:(proj1 (BQhalf_pos1 qa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)