transitivity z using LT.lt, LE.le
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < y + z
case zero_left.mp.left
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < z

case zero_left.mp.right
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ z ≤ y + z