cases Nat.le_total x z with
| inl h => rw [Nat.sub_eq_zero_of_le h, Nat.zero_add]; exact hz
| inr h => rw [Nat.add_comm, Nat.add_sub_comm, Nat.sub_eq_zero_of_le h, Nat.add_zero]; exact hx
case h
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z + z < y
no goals