cases i
m n i : Nat
hmn : m < n
hi : i > 0
⊢ m ^ i < n ^ i
case zero
m n : Nat
hmn : m < n
hi : zero > 0
⊢ m ^ zero < n ^ zero

case succ
m n : Nat
hmn : m < n
n✝ : Nat
hi : succ n✝ > 0
⊢ m ^ succ n✝ < n ^ succ n✝