constructor
case zero_left
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z ↔ 0 < y + z
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z → 0 < y + z

case zero_left.mpr
z : Nat
hz : z > 0
y : Nat
⊢ 0 < y + z → 0 < z