proposition: Theorem not_zerop_imp_in_newton_segment : ∀ f L f₁ L₁ r b, newton_segments f = Some L → f₁ = next_pol f (β L) (γ L) (ac_root (Φq f L)) → L₁ = option_get phony_ns (newton_segments f₁) → (∀ i : nat, i ≤ 1 → nth_r i f L = r) → (∀ n : nat, r ≤ nth_r n f L) → zerop_1st_n_const_coeff (S b) f₁ L₁ = false → ∀ n, n ≤ S b → newton_segments (nth_pol n f₁ L₁) = Some (nth_ns n f₁ L₁).
proof: Proof. intros f L f₁ L₁ r b HL Hf₁ HL₁ Hri Hrle Hz₁. remember (ac_root (Φq f L)) as c eqn:Hc. apply all_L_in_newton_segments with (r := r); try assumption. eapply next_ns_in_f; try eassumption. rewrite zerop_1st_n_const_coeff_succ in Hz₁. apply Bool.orb_false_iff in Hz₁. destruct Hz₁ as (Hz₁, Hpsi). simpl in Hz₁. remember (ps_poly_nth 0 f₁) as y. destruct (ps_zerop K y) as [| Hnz₁]; [ discriminate Hz₁ | subst y ]. assumption. pose proof (Hri 1%nat (Nat.le_refl 1)) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H; assumption. intros i. pose proof (Hrle (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