proposition: Theorem f₁_has_root : ∀ 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)) → ∃ s₁, (ps_pol_apply f₁ s₁ = 0)%ps.
proof: Proof. intros f L f₁ HL Hnz₀ Hf₁. remember (ac_root (Φq f L)) as c eqn:Hc. remember (root_multiplicity acf c (Φq f L)) as r eqn:Hr . symmetry in Hr. revert f L c f₁ HL Hnz₀ Hc Hf₁ Hr. induction r as (r, IHr) using lt_wf_rec; intros. set (v := fun i => if multiplicity_decreases f L i then S O else O). destruct (LPO v) as [Hn| Hn]. subst c. exists (f₁_root_when_r_constant f L). eapply root_for_f₁_when_r_constant; try eassumption. intros i. specialize (Hn i); unfold v in Hn. now destruct (multiplicity_decreases f L i). destruct Hn as (n, Hn). unfold v in Hn; clear v. unfold multiplicity_decreases in Hn. rewrite <- Hc, Hr in Hn. remember (nth_pol n f L) as fn eqn:Hfn . remember (nth_ns n f L) as Ln eqn:HLn . remember (nth_c n f L) as cn eqn:Hcn . remember (root_multiplicity acf cn (Φq fn Ln)) as rn eqn:Hrn . symmetry in Hrn. destruct (lt_dec rn r) as [Hrnr| Hrnr]; [ | now exfalso ]. destruct n. exfalso. simpl in Hfn, HLn, Hcn. subst fn Ln cn. rewrite <- Hc in Hrn. rewrite <- Hrn, Hr in Hrnr. now apply lt_irrefl in Hrnr. clear Hn; rename Hrnr into Hn. remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . erewrite <- nth_r_n in Hrn; try eassumption; subst rn. apply lowest_i_such_that_ri_lt_r₀ in Hn; [ | subst; auto ]. destruct Hn as (i, (Hin, (Hir, Hri))). destruct Hir as [Hir| Hir]. rewrite Hir, <- Hr, Hc in Hri. now apply Nat.lt_irrefl in Hri. destruct i. rewrite <- Hr, Hc in Hri. now apply Nat.lt_irrefl in Hri. remember (nth_pol i f L) as fi eqn:Hfi . remember (nth_ns i f L) as Li eqn:HLi . remember (nth_pol (S i) f L) as fsi eqn:Hfsi . remember (nth_ns (S i) f L) as Lsi eqn:HLsi . remember (newton_segments fsi) as Lo eqn:HLo . remember (nth_c (S i) f L) as cssi eqn:Hcssi. remember (next_pol fsi (β Lsi) (γ Lsi) cssi) as fssi eqn:Hfssi. symmetry in HLo. destruct Lo as [L₂| ]. remember (zerop_1st_n_const_coeff i f₁ L₁) as z eqn:Hz . symmetry in Hz. destruct z. apply lowest_zerop_1st_n_const_coeff in Hz. destruct Hz as (m, (Hm, (Hmi, (Hle, Heq)))). destruct Hle as [Hle| Hle]. move Hle at top; subst m. simpl in Heq. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₂| H₂]. exists 0%ps. apply a₀_0_root_0; assumption. discriminate Heq. exists (root_head 0 (pred m) f₁ L₁). apply root_when_fin; assumption. eapply IHr with (f := fsi) (L := Lsi) (f₁ := fssi) in Hri. destruct Hri as (s₁, Hs₁). remember (root_head 0 i f₁ L₁) as rh. remember (ps_monom 1%K (γ_sum 0 i f₁ L₁)) as mo. exists (rh + mo * s₁)%ps; subst rh mo. rewrite apply_nth_pol; auto with Arith. erewrite nth_pol_n; try eassumption; eauto . erewrite <- nth_c_n; try eassumption. rewrite <- Hcssi, <- Hfssi. rewrite Hs₁, rng_mul_0_r; reflexivity. subst Lsi. erewrite nth_ns_succ; [ | eassumption ]. now rewrite HLo. rewrite zerop_1st_n_const_coeff_false_iff in Hz. pose proof (Hz i (Nat.le_refl i)) as H. rewrite Hfsi; simpl. rewrite <- Hc, <- Hf₁, <- HL₁; auto with Arith. reflexivity. erewrite nth_c_n in Hcssi; try eassumption. rewrite <- Hcssi; assumption. symmetry. apply nth_r_n; try eassumption. erewrite nth_c_n; try eassumption; reflexivity. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₁| H₁]. apply a₀_0_root_0 in H₁. exists 0%ps; assumption. generalize HLo; intros H. rewrite Hfsi in H. simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H. apply nth_newton_segments_nil in H; auto with Arith. destruct H as (j, (Hjn, (Hjz, Hjnz))). destruct Hjz as [Hjz| Hjz]. subst j. simpl in Hjnz. destruct (ps_zerop K (ps_poly_nth 0 f₁)); [ contradiction | ]. discriminate Hjnz. exists (root_head 0 (pred j) f₁ L₁). apply root_when_fin; assumption. clear H. remember HL as H; clear HeqH. eapply next_has_root_0_or_newton_segments in H; auto with Arith. simpl in H. rewrite <- Hc, <- Hf₁ in H. destruct H; [ contradiction | ]. rewrite HL₁. now destruct (newton_segments f₁). 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