transitivity (y + (z - y)) using LE.le, LT.lt
case a
x y z : Nat
hx : x > y
hz : y < z
⊢ z < z - y + x
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ y + (z - y)

case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ y + (z - y) < z - y + x