This contains lemmas used by the Nat simprocs for simplifying arithmetic addition offsets.

theorem Nat.Simproc.sub_add_eq_comm (a : Nat) (b : Nat) (c : Nat) : a - (b + c) = a - c - b

theorem Nat.Simproc.add_sub_add_le (a : Nat) (c : Nat) {b : Nat} {d : Nat} (h : b ≤ d) : a + b - (c + d) = a - (c + (d - b))

theorem Nat.Simproc.add_sub_add_ge (a : Nat) (c : Nat) {b : Nat} {d : Nat} (h : b ≥ d) : a + b - (c + d) = a + (b - d) - c

theorem Nat.Simproc.add_sub_le (a : Nat) {b : Nat} {c : Nat} (h : b ≤ c) : a + b - c = a - (c - b)

theorem Nat.Simproc.add_eq_gt (a : Nat) {b : Nat} {c : Nat} (h : b > c) : (a + b = c) = False

theorem Nat.Simproc.eq_add_gt (a : Nat) {b : Nat} {c : Nat} (h : c > a) : (a = b + c) = False

theorem Nat.Simproc.add_eq_add_le (a : Nat) (c : Nat) {b : Nat} {d : Nat} (h : b ≤ d) : (a + b = c + d) = (a = c + (d - b))

theorem Nat.Simproc.add_eq_add_ge (a : Nat) (c : Nat) {b : Nat} {d : Nat} (h : b ≥ d) : (a + b = c + d) = (a + (b - d) = c)

theorem Nat.Simproc.add_eq_le (a : Nat) {b : Nat} {c : Nat} (h : b ≤ c) : (a + b = c) = (a = c - b)

theorem Nat.Simproc.eq_add_le {a : Nat} (b : Nat) {c : Nat} (h : c ≤ a) : (a = b + c) = (b = a - c)

theorem Nat.Simproc.beqEqOfEqEq {a : Nat} {b : Nat} {c : Nat} {d : Nat} (p : (a = b) = (c = d)) : (a == b) = (c == d)

theorem Nat.Simproc.beqFalseOfEqFalse {a : Nat} {b : Nat} (p : (a = b) = False) : (a == b) = false

theorem Nat.Simproc.bneEqOfEqEq {a : Nat} {b : Nat} {c : Nat} {d : Nat} (p : (a = b) = (c = d)) : (a != b) = (c != d)

theorem Nat.Simproc.bneTrueOfEqFalse {a : Nat} {b : Nat} (p : (a = b) = False) : (a != b) = true

theorem Nat.Simproc.add_le_add_le (a : Nat) (c : Nat) {b : Nat} {d : Nat} (h : b ≤ d) : (a + b ≤ c + d) = (a ≤ c + (d - b))

theorem Nat.Simproc.add_le_add_ge (a : Nat) (c : Nat) {b : Nat} {d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c)

theorem Nat.Simproc.add_le_le (a : Nat) {b : Nat} {c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b)

theorem Nat.Simproc.add_le_gt (a : Nat) {b : Nat} {c : Nat} (h : b > c) : (a + b ≤ c) = False

theorem Nat.Simproc.le_add_le (a : Nat) {b : Nat} {c : Nat} (h : a ≤ c) : (a ≤ b + c) = True

theorem Nat.Simproc.le_add_ge (a : Nat) {b : Nat} {c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b)