have : n^i > 0 := Nat.pos_pow_of_pos i (Nat.lt_of_succ_lt h)
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
⊢ succ i < n ^ succ i
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
this : n ^ i > 0
⊢ succ i < n ^ succ i