rw [Nat.add_comm, Nat.add_sub_comm, Nat.sub_eq_zero_of_le h, Nat.add_zero]
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x - z + z < y
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x < y