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