proposition: Theorem non_decr_imp_eq : ∀ 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 → nth_r n f L = r.
proof: Proof. intros f L b r HL Hz Hr Hri n Hnb. 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. remember Hz as H; clear HeqH. rewrite zerop_1st_n_const_coeff_succ2 in H. apply orb_false_iff in H. destruct H as (Hz₁, _). remember HL as H; clear HeqH. eapply all_L_in_newton_segments in H; try eassumption. rename H into HLni. remember (nth_ns n f L) as Ln eqn:HLn . remember (nth_pol n f L) as fn eqn:Hfn . remember (ac_root (Φq fn Ln)) as cn eqn:Hcn . remember (next_pol fn (β Ln) (γ Ln) cn) as fn₁ eqn:Hfn₁ . remember (option_get phony_ns (newton_segments fn₁)) as Ln₁ eqn:HLn₁ . remember (ac_root (Φq fn₁ Ln₁)) as cn₁ eqn:Hcn₁ . remember (nth_r (S n) f L) as r₁ eqn:Hr₁ . remember Hnb as H; clear HeqH. symmetry in Hr₁. apply Nat.succ_le_mono in H. rewrite zerop_1st_n_const_coeff_false_iff in Hz. apply Hz in H. erewrite nth_pol_succ in H; try eassumption; try reflexivity. erewrite nth_c_n in H; try eassumption. rewrite <- Hcn, <- Hfn₁ in H. rename H into Hnzn₁. remember HL as H; clear HeqH. eapply IHb in H; try eassumption. rename H into Hrn. remember Hcn as H; clear HeqH. erewrite <- nth_c_n in H; try eassumption. rename H into Hcnn. remember HLni as H; clear HeqH. eapply next_ns_r_non_decr with (r := r) (r₁ := r₁) in H; try eassumption. destruct H; symmetry; assumption. erewrite <- nth_r_n; try eassumption. symmetry; clear H. remember Hfn as H; clear HeqH. eapply nth_pol_succ in H; try eassumption. rewrite <- Hfn₁ in H. symmetry in H. rename H into Hfn₁₁. remember Hfn₁₁ as H; clear HeqH. eapply nth_ns_succ in H; try eassumption. rewrite <- HLn₁ in H. symmetry in H. rename H into HLn₁₁. erewrite nth_r_n in Hr₁; try eassumption; [ symmetry; eassumption | ]. erewrite nth_c_n; try eassumption. rewrite <- Hr₁; apply Hri. 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