proposition: Fact lmax_prop l x : In x l -> x <= lmax l.
proof: Proof. specialize (proj1 (lmax_spec l _) (Nat.le_refl _)). rewrite Forall_forall; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)