proposition: Fact lmax_spec l x : lmax l <= x <-> Forall (fun y => y <= x) l.
proof: Proof. revert x; induction l as [ | y l IHl ]; simpl. + split; auto; try lia. + intros x; rewrite Forall_cons_inv, <- IHl, Nat.max_lub_iff; tauto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)