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.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