case step j _ h_ind => calc
  n^i < n^j := h_ind
  _   ≤ n^j + n^j := Nat.le_add_left _ _
  _   = n^j*2 := (Nat.mul_two _).symm
  _   ≤ n^j*n := Nat.mul_le_mul_left _ hn
n i j✝ : Nat
hn : n ≥ 2
j : Nat
a✝ : Nat.le (succ i) j
h_ind : n ^ i < n ^ j
⊢ n ^ i < n ^ succ j
no goals