proposition: Lemma lee_sum_npos_ord (f : nat -> \bar R) (P : pred nat) : (forall n, P n -> f n <= 0) -> {homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
proof: Proof. move=> f0 m n ?; rewrite [leRHS](big_ord_widen_cond n) // big_mkcondr /=. by rewrite lee_sum // => i ?; case: ifP => // _; exact: f0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed