proposition: Lemma leR_sumR_Rabs (A : finType) f : `| \sum_a f a | <= \sum_(a : A) `| f a |.
proof: Proof. elim: (index_enum _) => [|h t IH]. by rewrite 2!big_nil Rabs_R0; exact: Rle_refl. rewrite 2!big_cons. apply (@leR_trans (`| f h | + `| \sum_(j <- t) f j |)); [exact/Rabs_triang |exact/leR_add2l]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)