a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ n + 1 < a ^ (n + 1)
a : ℕ
a1 : 1 < a
n : ℕ
⊢ n + 1 < a ^ (n + 1)
have IH := n_lt_a_pow n
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ (n + 1)
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ n + 1 < a ^ (n + 1)
have : a ^ n + a ^ n ≤ a ^ n * a := by
  rw [← mul_two]
  exact Nat.mul_le_mul_left _ a1
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n * a
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ (n + 1)
simp [_root_.pow_succ']
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n + a ^ n
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n * a
refine' lt_of_lt_of_le _ this
no goals
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
this : a ^ n + a ^ n ≤ a ^ n * a
⊢ n + 1 < a ^ n + a ^ n
exact add_lt_add_of_lt_of_le IH (lt_of_le_of_lt (Nat.zero_le _) IH)
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ a ^ n * 2 ≤ a ^ n * a
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ a ^ n + a ^ n ≤ a ^ n * a
rw [← mul_two]
no goals
a : ℕ
a1 : 1 < a
n : ℕ
IH : n < a ^ n
⊢ a ^ n * 2 ≤ a ^ n * a
exact Nat.mul_le_mul_left _ a1