n a q : ℕ
a0 : 0 < a
q1 : 1 < q
⊢ n < a * q ^ n
n a q : ℕ
a0 : 0 < a
q1 : 1 < q
⊢ n * q < a * q ^ (n + 1)
rw [pow_succ, ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)]
no goals
n a q : ℕ
a0 : 0 < a
q1 : 1 < q
⊢ n < a * q ^ n
exact lt_mul_of_one_le_of_lt (Nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n)