proposition: Lemma lee_dsum_npos_natr (f : nat -> \bar^d R) (P : pred nat) m : (forall n, (m <= n)%N -> P n -> f n <= 0) -> {homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
proof: Proof. move=> f0 i j le_ij; rewrite !dual_sumeE leeN2. apply: lee_sum_nneg_natr => [n ? ?|//]; rewrite oppe_ge0; exact: f0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed