no goals
m✝ n m : ℕ
⊢ m ! * succ m ^ 0 ≤ (m + 0)!
simp
m✝ n✝ m n : ℕ
⊢ m ! * succ m ^ n * succ m ≤ (m + n)! * (m + n + 1)
m✝ n✝ m n : ℕ
⊢ m ! * succ m ^ (n + 1) ≤ (m + (n + 1))!
rw [← add_assoc, ← Nat.succ_eq_add_one (m + n), Nat.factorial_succ, pow_succ',
    mul_comm (_ + 1), mul_comm (succ m), ← mul_assoc]
no goals
m✝ n✝ m n : ℕ
⊢ m ! * succ m ^ n * succ m ≤ (m + n)! * (m + n + 1)
exact
  mul_le_mul factorial_mul_pow_le_factorial (Nat.succ_le_succ (Nat.le_add_right _ _))
    (Nat.zero_le _) (Nat.zero_le _)