proposition: Lemma qsum_even_odd f n: natp n -> rat_below f (cdouble n) -> qsum f (cdouble n) = qsum (fun i => f (cdouble i)) n +q qsum (fun i => f (csucc(cdouble i))) n.
proof: Proof. move: n; apply: Nat_induction; first by rewrite cdouble0 !qsum0 (BQsum_0r QS0). move => n nN Hrec fp. move: (NS_double nN) => dN; move:(NS_succ dN) (NS_succ nN) => sdN snN. move: (cltS nN) => lt1. move/(double_monotone2 nN snN): (lt1) => lt2. have ha: inc (f (cdouble n)) BQ by apply:fp. have hb: inc (f (csucc (cdouble n))) BQ. by apply:fp; apply /(double_monotone3 nN snN). have hc:inc (qsum (fun i => f (cdouble i)) n) BQ. apply:(QS_qsum nN) => i lin;apply: fp. apply /(double_monotone2 (NS_lt_nat lin nN) snN); exact: (clt_ltT lin lt1). have hd: inc (qsum (fun i => f (csucc (cdouble i))) n) BQ. apply:(QS_qsum nN) => i lin;apply: fp. apply /(double_monotone3 (NS_lt_nat lin nN) snN); exact: (clt_ltT lin lt1). have he: rat_below f (cdouble n). move=> i lin;apply: fp; exact: (clt_ltT lin lt2). have hf:=(QS_qsum dN he). rewrite (double_succ nN) (qsum_rec _ sdN) (qsum_rec _ dN) ! (qsum_rec _ nN). rewrite (BQsum_ACA ha hc hb hd) (BQsumA hb ha hf) (BQsumC (f _)) Hrec //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)