induction hij
n i j : Nat
hn : n ≥ 2
hij : i < j
⊢ n ^ i < n ^ j
case refl
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i

case step
n i j : Nat
hn : n ≥ 2
m✝ : Nat
a✝ : Nat.le (succ i) m✝
a_ih✝ : n ^ i < n ^ m✝
⊢ n ^ i < n ^ succ m✝