case succ i h_ind =>
have : n^i > 0 := Nat.pos_pow_of_pos i (Nat.lt_of_succ_lt h)
calc
  i+1 < n^i + 1 := succ_lt_succ h_ind
  _   ≤ n^i + n^i := Nat.add_le_add_left this _
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left _ h
  _   = n^(i+1) := rfl
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
⊢ succ i < n ^ succ i
no goals