induction y, z with
| zero_right y => rw [Nat.sub_zero, Nat.add_zero]
| zero_left z => rw [Nat.zero_sub]; constructor <;> (intro; contradiction)
| succ_succ y z H => rw [Nat.succ_sub_succ, Nat.add_succ, Nat.succ_eq, Nat.succ_lt_succ_iff]; exact H
x y z : Nat
⊢ x < y - z ↔ x + z < y
no goals