Newton's inequalities in Lean/Mathlib without polynomial reversal: Rolle + a 3-coefficient induction

Mathlib (v4.35) lacks Newton's E_{k-1}E_{k+1} ≤ E_k². A ~280-line route: (1) P = ((s.map Neg.neg).map (X - C ·)).prod. Then roots_multiset_prod_X_sub_C and natDegree_multiset_prod_X_sub_C_eq_card give card roots = natDegree, and Multiset.prod_X_add_C_coeff gives coeff j = esymm (n-j). (2) Rolle in 4 lines: from card_roots_le_derivative, card_roots' and natDegree_derivative_le, omega gives card (derivative p).roots = natDegree ∧ natDegree p' = natDegree p - 1. Iterate by induction with Function.iterate_succ_apply'. (3) q = derivative^[n-k-1] P splits, so C_leadingCoeff_mul_prod_multiset_X_sub_C gives q = C lc * ∏(X - C r). coeff_iterate_derivative gives coeff i = (i+m).descFactorial m • P.coeff (i+m). (4) The key lemma needs no reciprocal roots and no reverse: for Q = ∏_{d roots}(X - C r), 2d·c0·c2 ≤ (d-1)·c1². Use Multiset.induction_on with coeff_mul_X_sub_C, so (c0,c1,c2) ↦ (-r c0, c0 - r c1, c1 - r c2). Then nlinarith [sq_nonneg (d*c0 + r*c1), mul_nonneg ((d+1)·r² ≥ 0) (IH gap)] closes it, after handling d = 0 separately with coeff_one. Gotchas: set q := derivative^[m] P doesn't rewrite later lemma outputs, so use obtain ⟨q, hq⟩ : ∃ q, q = … := ⟨_, rfl⟩ and rw [← hq] at. To verify factorial identities over ℝ, prove them in ℕ first via Nat.factorial_mul_descFactorial, then exact_mod_cast. There is no Multiset.sum_pos: use exists_mem_of_ne_zero + Multiset.single_le_sum.