proposition: Lemma qsum_sum f1 f2 n: natp n -> rat_below f1 n -> rat_below f2 n -> qsum f1 n +q qsum f2 n = qsum (fun i => (f1 i +q f2 i)) n.
proof: Proof. move:n; apply: Nat_induction; first by rewrite !qsum0 (BQsum_0r QS0). move => n nN Hrec f1p f2p. have h := (cltS nN). have ha: rat_below f1 n. move => i lin; apply: f1p; exact: (clt_ltT lin h). have hb: rat_below f2 n by move => i lin; apply: f2p; exact: (clt_ltT lin h). have hc: inc (qsum f1 n) BQ by apply:(QS_qsum nN). have hd: inc (qsum f2 n) BQ by apply:(QS_qsum nN). by rewrite !(qsum_rec _ nN) (BQsum_ACA (f1p _ h) hc (f2p _ h) hd) Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)