no goals
n : ℕ
⊢ (n + 1) ^ 0 ≤ ascFactorial n 0
rw [ascFactorial_zero, pow_zero]
n k : ℕ
⊢ (n + 1) * (n + 1) ^ k ≤ ascFactorial n (k + 1)
n k : ℕ
⊢ (n + 1) ^ (k + 1) ≤ ascFactorial n (k + 1)
rw [pow_succ, mul_comm]
no goals
n k : ℕ
⊢ (n + 1) * (n + 1) ^ k ≤ ascFactorial n (k + 1)
exact Nat.mul_le_mul (Nat.add_le_add_right le_self_add _) (pow_succ_le_ascFactorial _ k)