proposition: Lemma qsum_An1 f m: natp m -> (rat_below f (csucc m)) -> qsum f (csucc m) = (f \0c) +q (qsum (fun i => f (csucc i)) m).
proof: Proof. move => mN Ha. have f0q: inc (f \0c) BQ by apply: Ha; apply: succ_positive. move: Ha; rewrite (Nsucc_rw mN) csumC => Ha. rewrite (qsum_An NS1 mN Ha) (qsum1 f0q); congr( _ +q _). by apply:(qsum_exten mN) => i lim; rewrite (Nsucc_rw (NS_lt_nat lim mN)) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)