refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _)
case h
n i : ℕ
x : ℝ
⊢ ↑(Nat.descFactorial n i) * ‖x ^ (n - i)‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
case h
n i : ℕ
x : ℝ
⊢ ‖x ^ (n - i)‖ ≤ (1 + ‖x‖) ^ (n - i)