proposition: Lemma CR_prop4 n: natp n -> inc (qsum (CR_next_term f) n) BQp.
proof: Proof. move: n; apply: Nat_induction; first by rewrite qsum0; apply: QpS0. move => n nN hr; rewrite (qsum_rec _ nN); apply: QpS_sum hr. by apply: CR_prop3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)