proposition: Lemma qsum_An f n m: natp n -> natp m -> (rat_below f (n +c m)) -> qsum f (n +c m) = (qsum f n) +q (qsum (fun i => f (n +c i)) m).
proof: Proof. move => nN hb; move: m hb; apply: Nat_induction. by rewrite (Nsum0r nN) qsum0 => /(QS_qsum nN) sq; rewrite BQsum_0r. move => m mN Hrec h1. have ha := (NS_sum nN mN). have hb: inc (f (n +c m)) BQ by apply: h1; rewrite (csum_nS _ mN);apply: cltS. have hc: inc (qsum f n) BQ. apply:(QS_qsum nN) => i lin; apply: h1; rewrite (csum_nS n mN). exact: (clt_ltT (clt_leT lin (csum_M0le m (CS_nat nN))) (cltS ha)). have hd: inc (qsum (fun i => f (n +c i)) m) BQ. apply:(QS_qsum mN) => i lin; apply: h1. apply:(csum_Meqlt nN); exact: (clt_ltT lin (cltS mN)). have he: forall i, i <c n +c m -> inc (f i) BQ. move => i lin; apply: h1;rewrite (csum_nS n mN). exact: (clt_ltT lin (cltS ha)). rewrite (csum_nS _ mN) (qsum_rec _ ha) (Hrec he) (qsum_rec _ mN). rewrite (BQsumA hb hc hd) (BQsumA hc hb hd) (BQsumC (f (n +c m))) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)