proposition: Lemma lee_sum_nneg_natr (f : nat -> \bar R) (P : pred nat) m : (forall n, (m <= n)%N -> P n -> 0 <= f n) -> {homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}.
proof: Proof. move=> f0 i j le_ij; rewrite -[m]add0n !big_addn !big_mkord. apply: (@lee_sum_nneg_ord (fun k => f (k + m)%N) (fun k => P (k + m)%N)); by [move=> n /f0; apply; rewrite leq_addl | rewrite leq_sub2r]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed