proposition: Lemma qsum_one f n: natp n -> (forall i, i<c n -> f i = \1q) -> qsum f n = BQ_of_nat n.
proof: Proof. move: n; apply: Nat_induction; first by move => _; rewrite qsum0. move => n nN Hrec fp; move: (cltS nN) => aux. rewrite (qsum_rec _ nN)(Nsucc_rw nN) csumC - (BQsum_cN NS1 nN) (fp _ aux). congr (_ +q _); apply: Hrec => i lin; apply: fp; apply:(clt_ltT lin aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)