proposition: Lemma CR_prop6 n : natp n -> CR_partial_sum f (csucc n) <=q CR_partial_sum f n +q (CR_inv3n (csucc n)).
proof: Proof. move => nN; rewrite /CR_partial_sum (qsum_rec _ (NS_succ nN)). have ha:= (CR_prop0 (NS_succ nN)). have hb:= (CR_prop3 (NS_succ nN)). have hc:= (proj31 (CR_prop5 nN)). rewrite BQsumC; apply/(BQsum_le2l (BQp_sBQ hb) (BQps_sBQ ha) hc). case: (CR_prop2 (NS_succ nN)) => ->. apply/ qle0xP; apply: (BQps_sBQp ha). apply: (qleR (BQps_sBQ ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)