proposition: Lemma CR_prop9 n: natp n -> inc (CR_partial_sum f n +q (CR_inv3n n)) (CR_limit f).
proof: Proof. move => nN. move:(CR_prop6 nN) => eq1. move:(CR_prop5 nN) => [xq yq _]. move: (CR_prop1 nN) (CR_prop1 (NS_succ nN)) => cc cc1. move: (QSdouble cc1) => cc2. apply: (Zo_i (QSs xq cc)); exists (csucc n); first by apply: (NS_succ nN). move/ (BQsum_le2r yq (proj32 eq1) cc1): eq1 => eq2; apply:(qle_ltT eq2). rewrite - (BQsumA xq cc1 cc1) (BQdouble_p cc1) (CR_prop00 nN). rewrite - (BQ_double_plus cc1) (BQsumA xq cc2 cc1). apply:(BQsum_Mps (QSs xq cc2)) (CR_prop0 (NS_succ nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)