proposition: Lemma qsum_rev f n: natp n -> rat_below f n -> qsum f n = qsum (fun i => f (n -c (csucc i))) n.
proof: Proof. move => nN; move: n nN f; apply: Nat_induction. by move => f _; rewrite !qsum0. move => n nN Hrec f fp; move: (cltS nN) => sa. have ->: qsum (fun i => f (csucc n -c csucc i)) (csucc n) = qsum (fun i => f (n -c i)) (csucc n). apply:(qsum_exten (NS_succ nN)) => i lin; rewrite cdiff_pr6 //. by apply: (NS_lt_nat lin (NS_succ nN)). have ha: forall i, i <c csucc n -> inc (f (n -c i)) BQ. move => i lin; apply: fp; apply /(cltSleP nN); apply:cdiff_le1; fprops. rewrite (qsum_rec _ nN) (qsum_An1 nN ha) (cdiff_n0 nN) Hrec //. by move => i lin;apply: fp; apply:(clt_ltT lin sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)