transitivity 1 using LT.lt
case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0
case succ_succ.hk.left
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 0 < 1

case succ_succ.hk.right
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 1 < z