proposition: Lemma lee_sum_nneg_natl (f : nat -> \bar R) (P : pred nat) n : (forall m, (m < n)%N -> P m -> 0 <= f m) -> {homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
proof: Proof. move=> f0 i j le_ij; rewrite !big_geq_mkord/=. rewrite lee_sum_nneg_subset// => [k | k /and3P[_ /f0->//]]. by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed