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