theorem Nat.succ_sub {m : Nat} {n : Nat} (h : n ≤ m) : Nat.succ m - n = Nat.succ (m - n)

theorem Nat.sub_le_sub_right {n : Nat} {m : Nat} (h : n ≤ m) (k : Nat) : n - k ≤ m - k

theorem Nat.sub_lt_left_of_lt_add {n : Nat} {k : Nat} {m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m

theorem Nat.sub_lt_right_of_lt_add {n : Nat} {k : Nat} {m : Nat} (H : n ≤ k) (h : k < m + n) : k - n < m

theorem Nat.pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n

theorem Nat.min_eq_min {b : Nat} (a : Nat) : Nat.min a b = min a b

theorem Nat.max_eq_max {b : Nat} (a : Nat) : Nat.max a b = max a b

theorem Nat.min_comm (a : Nat) (b : Nat) : min a b = min b a

theorem Nat.min_le_right (a : Nat) (b : Nat) : min a b ≤ b

theorem Nat.min_le_left (a : Nat) (b : Nat) : min a b ≤ a

theorem Nat.min_eq_left {a : Nat} {b : Nat} (h : a ≤ b) : min a b = a

theorem Nat.min_eq_right {a : Nat} {b : Nat} (h : b ≤ a) : min a b = b

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

theorem Nat.le_max_left (a : Nat) (b : Nat) : a ≤ max a b

theorem Nat.le_max_right (a : Nat) (b : Nat) : b ≤ max a b

theorem Nat.pow_two_pos (w : Nat) : 0 < 2 ^ w

@[simp]

theorem Nat.not_le {a : Nat} {b : Nat} : ¬a ≤ b ↔ b < a

@[simp]

theorem Nat.not_lt {a : Nat} {b : Nat} : ¬a < b ↔ b ≤ a

theorem Nat.le_min_of_le_of_le {a : Nat} {b : Nat} {c : Nat} : a ≤ b → a ≤ c → a ≤ min b c

theorem Nat.le_min {a : Nat} {b : Nat} {c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

theorem Nat.lt_min {a : Nat} {b : Nat} {c : Nat} : a < min b c ↔ a < b ∧ a < c