proposition: Lemma CR_prop5 n : natp n -> CR_partial_sum f n <=q CR_partial_sum f (csucc n).
proof: Proof. move => nN; rewrite /CR_partial_sum (qsum_rec _ (NS_succ nN)). have pa:= (CR_prop3 (NS_succ nN)). have pb:=(BQp_sBQ (CR_prop4 (NS_succ nN))). rewrite BQsumC; apply:(BQsum_Mp pb pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)