proposition: Theorem all_L_in_newton_segments : ∀ f L b r, newton_segments f = Some L → zerop_1st_n_const_coeff b f L = false → nth_r 0 f L = r → (∀ i, r ≤ nth_r i f L) → ∀ n : nat, n ≤ b → newton_segments (nth_pol n f L) = Some (nth_ns n f L).
proof: Proof. intros f L b r HL Hz Hr Hri n Hnb. rewrite zerop_1st_n_const_coeff_false_iff in Hz. revert f L n HL Hz Hr Hri Hnb. induction b; intros; [ apply Nat.le_0_r in Hnb; subst n; assumption | ]. destruct n; [ assumption | ]. apply le_S_n in Hnb; simpl. remember (ac_root (Φq f L)) as c eqn:Hc . remember (next_pol f (β L) (γ L) c) as f₁ eqn:Hf₁ . remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . apply IHb; try assumption. eapply nth_in_newton_segments_any_r with (n := 1%nat); try eassumption. intros i Hi1. apply Hz. transitivity 1%nat; [ assumption | apply le_n_S, Nat.le_0_l ]. simpl; rewrite <- Hc; assumption. simpl; rewrite <- Hc, <- Hf₁; assumption. intros i Hib. apply Nat.succ_le_mono in Hib. apply Hz in Hib; simpl in Hib. rewrite <- Hc, <- Hf₁, <- HL₁ in Hib; assumption. simpl in Hr; rewrite <- Hc in Hr. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . remember (root_multiplicity acf c₁ (Φq f₁ L₁)) as r₁ eqn:Hr₁ . remember HL as H; clear HeqH. symmetry in Hr₁. eapply next_ns_r_non_decr in H; try eassumption. destruct H as (H, _); move H at top; subst r₁. simpl; rewrite <- Hc₁; assumption. clear H. assert (1 ≤ S b)%nat as H by apply le_n_S, Nat.le_0_l. apply Hz in H; simpl in H. rewrite <- Hc, <- Hf₁ in H; assumption. clear H. pose proof (Hri 1%nat) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁, Hr₁ in H; assumption. intros i. pose proof (Hri (S i)) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H; 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