proposition: Theorem no_newton_segments : ∀ f, (ps_poly_nth 0 f ≠ 0)%ps → newton_segments f = None → (∀ i, (0 < i)%nat → (ps_poly_nth i f = 0)%ps).
proof: Proof. intros f Hnz HL i Hi. destruct i; [ exfalso; revert Hi; apply Nat.lt_irrefl | idtac ]. clear Hi. unfold newton_segments in HL. unfold lower_convex_hull_points in HL. unfold points_of_ps_polynom in HL. unfold points_of_ps_lap in HL. remember (al f) as la eqn:Hla . symmetry in Hla. unfold ps_poly_nth. unfold ps_poly_nth in Hnz. rewrite Hla in Hnz; rewrite Hla. clear f Hla. unfold points_of_ps_lap_gen in HL. unfold qpower_list in HL. remember (pair_rec (λ pow ps, (Qnat pow, ps))) as f. unfold ps_lap_nth in Hnz. unfold ps_lap_nth. revert la Hnz HL. induction i; intros. destruct la as [| a]. exfalso; apply Hnz; reflexivity. simpl in Hnz; simpl. simpl in HL. remember (f (O, a)) as fa. rewrite Heqf in Heqfa. simpl in Heqfa. unfold pair_rec in Heqfa; simpl in Heqfa. subst fa; simpl in HL. apply order_fin in Hnz. remember (order a) as oa. symmetry in Heqoa. destruct oa as [oa| ]; [ idtac | exfalso; apply Hnz; reflexivity ]. simpl in HL. remember (filter_finite_ord (List.map f (power_list 1 la))) as pts. symmetry in Heqpts. destruct pts; [ idtac | discriminate HL ]. clear HL Hnz. destruct la as [| b]; [ reflexivity | simpl ]. simpl in Heqpts. remember (f (1%nat, b)) as fb. rewrite Heqf in Heqfb. unfold pair_rec in Heqfb. simpl in Heqfb. subst fb; simpl in Heqpts. remember (order b) as ob. symmetry in Heqob. destruct ob as [ob| ]; auto. discriminate Heqpts. apply order_inf; assumption. destruct la as [| a]; [ reflexivity | simpl ]. simpl in Hnz. simpl in HL. remember (f (O, a)) as fa. rewrite Heqf in Heqfa. simpl in Heqfa. unfold pair_rec in Heqfa; simpl in Heqfa. subst fa; simpl in HL. apply order_fin in Hnz. remember (order a) as oa. symmetry in Heqoa. destruct oa as [oa| ]; [ idtac | exfalso; apply Hnz; reflexivity ]. simpl in HL. remember (filter_finite_ord (List.map f (power_list 1 la))) as pts. symmetry in Heqpts. destruct pts; [ idtac | discriminate HL ]. clear HL. clear Hnz. revert Heqf Heqpts; clear; intros. remember 1%nat as pow; clear Heqpow. revert i pow Heqpts. induction la as [| a]; intros; [ reflexivity | idtac ]. simpl in Heqpts. remember (f (pow, a)) as fa. rewrite Heqf in Heqfa. unfold pair_rec in Heqfa. simpl in Heqfa. subst fa; simpl in Heqpts. remember (order a) as oa. symmetry in Heqoa. destruct oa as [oa| ]; [ discriminate Heqpts | simpl ]. destruct i. destruct la as [| b]; [ reflexivity | simpl ]. simpl in Heqpts. remember (f (S pow, b)) as fb. rewrite Heqf in Heqfb. unfold pair_rec in Heqfb; simpl in Heqfb. subst fb. apply order_inf. remember (order b) as ob. symmetry in Heqob. destruct ob as [ob| ]; [ discriminate Heqpts | reflexivity ]. eapply IHla; eauto . Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM