proposition: Fact lsum_le x l : In x l -> x <= lsum l.
proof: Proof. intros H; apply in_split in H. destruct H as (u & v & ->). rewrite lsum_app; simpl; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)