rw [Nat.succ_sub_succ, Nat.succ_add, Nat.succ_eq, Nat.succ_lt_succ_iff]
case succ_succ
z : Nat
hz : z > 0
x y : Nat
H : x - y < z ↔ x < y + z
⊢ x + 1 - (y + 1) < z ↔ x + 1 < y + 1 + z
case succ_succ
z : Nat
hz : z > 0
x y : Nat
H : x - y < z ↔ x < y + z
⊢ x - y < z ↔ x < y + z