proposition: Lemma QS_qsum f n: natp n -> rat_below f n -> ratp (qsum f n).
proof: Proof. move:n;apply: Nat_induction. move => _; rewrite qsum0; apply: QS0. move => n nN Hrec h1; rewrite (qsum_rec f nN); apply: QSs. by apply: h1; apply: cltS. by apply: Hrec => i [/(cltSleP nN) /h1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)