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