proposition: Theorem next_has_root_0_or_newton_segments : ∀ f L c f₁, newton_segments f = Some L → c = ac_root (Φq f L) → f₁ = nth_pol 1 f L → (ps_poly_nth 0 f₁ = 0)%ps ∨ (newton_segments f₁ ≠ None).
proof: Proof. intros f L c f₁ HL Hc Hf₁. remember HL as H; clear HeqH. eapply f₁_orders in H; try eassumption; try apply eq_refl. simpl in Hf₁. rewrite <- Hc in Hf₁. rewrite <- Hf₁ in H. remember (root_multiplicity acf c (Φq f L)) as r eqn:Hr . symmetry in Hr. destruct H as (Hnneg, (Hpos, Hz)). destruct r. exfalso; revert Hr. apply multiplicity_neq_0; assumption. pose proof (Hpos O (Nat.lt_0_succ r)) as H₂. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₁| H₁]. left; assumption. right. apply order_fin in H₁; intros H. unfold newton_segments in H. unfold points_of_ps_polynom in H. unfold points_of_ps_lap in H. unfold points_of_ps_lap_gen in H. unfold qpower_list in H. unfold ps_poly_nth in Hz, H₁. remember (al f₁) as la; clear Heqla. unfold ps_lap_nth in Hz, H₁. destruct la as [| a]. simpl in Hz. rewrite order_0 in Hz; inversion Hz. simpl in Hz, H₁, H. remember (order a) as oa eqn:Hoa . symmetry in Hoa. destruct oa as [oa| ]. remember 1%nat as pow. assert (1 ≤ pow)%nat as Hpow by (subst pow; apply Nat.le_refl). clear Heqpow Hr Hpos a Hoa. revert r pow H Hz Hpow. induction la as [| a]; intros. simpl in Hz. rewrite match_id in Hz. rewrite order_0 in Hz; inversion Hz. simpl in Hz. destruct r. simpl in H. remember (order a) as oa₁ eqn:Hoa . symmetry in Hoa. destruct oa₁ as [oa₁| ]. unfold lower_convex_hull_points in H. discriminate H. inversion Hz. simpl in H. remember (order a) as oa₁ eqn:Hoa . symmetry in Hoa. destruct oa₁ as [oa₁| ]. unfold lower_convex_hull_points in H. discriminate H. eapply IHla; try eassumption; apply le_n_S, Nat.le_0_l. apply H₁; reflexivity. 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