case refl => calc
  n^i < n^i + n^i := Nat.lt_add_of_pos_left (Nat.pos_pow_of_pos i (trans (Nat.zero_lt_succ 1) hn))
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left (n^i) hn
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i
no goals