proposition: Theorem root_for_f₁_when_r_constant : ∀ f L f₁, newton_segments f = Some L → (ps_poly_nth 0 f ≠ 0)%ps → f₁ = next_pol f (β L) (γ L) (ac_root (Φq f L)) → (∀ i, if multiplicity_decreases f L i then False else True) → (ps_pol_apply f₁ (f₁_root_when_r_constant f L) = 0)%ps.
proof: Proof. intros f L f₁ HL Hnz₀ Hf₁ Hn. unfold f₁_root_when_r_constant. rewrite <- Hf₁. remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁. remember (ac_root (Φq f L)) as c eqn:Hc in Hf₁. remember (ps_pol_com_polydo f) as m eqn:Hm. remember (q_of_m m (γ L)) as q₀ eqn:Hq₀ . remember (root_tail (m * q₀) 0 f₁ L₁) as s eqn:Hs . destruct (fld_zerop 1%K) as [H₀| H₀]. unfold ps_pol_apply, apply_poly, apply_lap; simpl. destruct (al f₁) as [| a]; [ reflexivity | simpl ]. rewrite rng_mul_0_r, rng_add_0_l. apply eq_1_0_ps_0; assumption. remember (order (ps_pol_apply f₁ s)) as ofs eqn:Hofs . destruct ofs as [ofs| ]. remember (Z.to_nat (2 * Zpos m * Zpos q₀ * Qnum ofs)) as N eqn:HN . remember (zerop_1st_n_const_coeff N f₁ L₁) as z eqn:Hz . symmetry in Hz. destruct z. apply lowest_zerop_1st_n_const_coeff in Hz. destruct Hz as (i, (Hi, (Hin, (Hji, Hz)))). symmetry in Hi. rewrite Hi. destruct Hji as [Hi2| Hpi]. move Hi2 at top; subst i. simpl in Hz. destruct (ps_zerop K (ps_poly_nth 0 f₁)); [ | discriminate Hz ]. apply a₀_0_root_0; assumption. destruct i. simpl in Hpi, Hz; rewrite Hpi in Hz; discriminate Hz. apply root_when_fin in Hpi; [ apply Hpi | assumption ]. exfalso. remember (root_multiplicity acf c (Φq f L)) as r eqn:Hr . symmetry in Hr. pose proof (multiplicity_neq_0 acf f HL Hc) as H. destruct r; [ contradiction | ]. revert Hz; apply not_false_iff_true. eapply upper_bound_zerop_1st_when_r_constant; try eassumption. rewrite Hofs, Hs; reflexivity. symmetry in Hofs. apply order_inf; assumption. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail RootAnyR