proposition: Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I -> \bar^d R) (P : pred I) : `|\sum_(i <- s | P i) F i| <= \sum_(i <- s | P i) `|F i|.
proof: Proof. elim/big_ind2 : _ => //; first by rewrite abse0. by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dadd _ _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed