HepLean Documentation

Init.Data.Nat.Simproc

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)