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
this : n ^ i > 0
⊢ succ i < n ^ succ i
no goals