proposition: Fact lsum_app l r : lsum (l++r) = lsum l+lsum r.
proof: Proof. induction l as [ | x l IHl ]; simpl; auto; rewrite IHl; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)