ink

theorem Mt.Utils.Nat.max_of_le {a : Nat} {b : Nat} : a ≤ b → Nat.max a b = b

ink

theorem Mt.Utils.Nat.max_of_eq' {a : Nat} {b : Nat} : a = b → Nat.max a b = b

ink

theorem Mt.Utils.Nat.max_of_eq {a : Nat} {b : Nat} : a = b → Nat.max a b = a

ink

theorem Mt.Utils.Nat.max_of_gt {a : Nat} {b : Nat} : a > b → Nat.max a b = a

ink

theorem Mt.Utils.Nat.max_of_ge {a : Nat} {b : Nat} : a ≥ b → Nat.max a b = a

ink

theorem Mt.Utils.Nat.max_of_lt {a : Nat} {b : Nat} : a < b → Nat.max a b = b

ink

theorem Mt.Utils.Nat.max_comm (a : Nat) (b : Nat) : Nat.max a b = Nat.max b a

ink

theorem Mt.Utils.Nat.max_assoc (a : Nat) (b : Nat) (c : Nat) : Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

ink

theorem Mt.Utils.Nat.zero_max (a : Nat) : Nat.max 0 a = a

ink

theorem Mt.Utils.Nat.max_zero (a : Nat) : Nat.max a 0 = a

ink

theorem Mt.Utils.Nat.max_le {a : Nat} {b : Nat} {c : Nat} : Nat.max a b ≤ c ↔ a ≤ c ∧ b ≤ c