transitivity (1 * (x + 1)) using Eq, LE.le
case succ_succ
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 ≤ (x + 1) ^ (y + 1)
case succ_succ.left
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 = 1 * (x + 1)

case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ (y + 1)