proposition: Theorem nth_newton_segments_nil : ∀ f L n, newton_segments f = Some L → newton_segments (nth_pol n f L) = None → (∃ i, i ≤ n ∧ (i = O ∨ zerop_1st_n_const_coeff (pred i) f L = false) ∧ zerop_1st_n_const_coeff i f L = true).
proof: Proof. intros f L n HL HLe. revert f L HL HLe. induction n; intros. now simpl in HLe; rewrite HLe in HL. simpl in HLe. remember HL as H; clear HeqH. eapply next_has_root_0_or_newton_segments in H; try apply eq_refl. destruct H as [H| H]. simpl in H. 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₁ . destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]. exists 0%nat. split; [ apply Nat.le_0_l | idtac ]. split; [ left; reflexivity | simpl ]. destruct (ps_zerop K (ps_poly_nth 0 f)); [ | contradiction ]. apply eq_refl. exists 1%nat. split; [ apply le_n_S, Nat.le_0_l | idtac ]. split. right; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); [ contradiction | ]. apply eq_refl. simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); [ apply eq_refl | ]. rewrite <- Hc, <- Hf₁. destruct (ps_zerop K (ps_poly_nth 0 f₁)); [ | contradiction ]. apply eq_refl. simpl in H. 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₁ . rename H into HLe₁. remember HLe as H; clear HeqH. apply IHn in H. destruct H as (i, (Hin, (Hiz, Hinz))). destruct Hiz as [Hiz| Hiz]. subst i. simpl in Hinz. destruct (ps_zerop K (ps_poly_nth 0 f₁)). destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₂| H₂]. exists 0%nat. split; [ apply Nat.le_0_l | idtac ]. split; [ left; reflexivity | simpl ]. destruct (ps_zerop K (ps_poly_nth 0 f)); [ | contradiction ]. apply eq_refl. exists 1%nat. split; [ apply le_n_S, Nat.le_0_l | idtac ]. split. right; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); [ | apply eq_refl ]. contradiction. simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); [ apply eq_refl | ]. rewrite <- Hc, <- Hf₁. destruct (ps_zerop K (ps_poly_nth 0 f₁)); [ | contradiction ]. apply eq_refl. discriminate Hinz. destruct i. rewrite Nat.pred_0 in Hiz. rewrite Hinz in Hiz; discriminate Hiz. rewrite Nat.pred_succ in Hiz. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]. exists 0%nat. split; [ apply Nat.le_0_l | idtac ]. split; [ left; reflexivity | simpl ]. destruct (ps_zerop K (ps_poly_nth 0 f)); [ | contradiction ]. apply eq_refl. exists (S (S i)). split; [ apply Nat.succ_le_mono in Hin; assumption | idtac ]. split. right; rewrite Nat.pred_succ. simpl. destruct (ps_zerop K (ps_poly_nth 0 f)). contradiction. rewrite <- Hc, <- Hf₁, <- HL₁. assumption. remember (S i) as si; simpl; subst si. destruct (ps_zerop K (ps_poly_nth 0 f)). reflexivity. rewrite <- Hc, <- Hf₁, <- HL₁. assumption. rewrite HL₁. now destruct (newton_segments f₁). 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