proposition: Lemma list_sum_map_le {X: Type} f g (L: list X) : (forall x, f x <= g x) -> list_sum (map f L) <= list_sum (map g L).
proof: Proof. move=> Hfg. elim: L; first done. move=> x L IH /=. have := Hfg x. lia. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun