proposition: Theorem hd_newton_segments : ∀ f L j k αj αk, L = option_get phony_ns (newton_segments f) → ini_pt L = (Qnat j, αj) → fin_pt L = (Qnat k, αk) → (j < k)%nat → newton_segments f = Some L.
proof: Proof. intros f L j k αj αk HL Hini Hfin Hjk. remember (newton_segments f) as Ll. symmetry in HeqLl. destruct Ll as [L₁| ]; simpl in HL. subst L; reflexivity. subst L; simpl in Hini, Hfin. injection Hini; intros; subst. injection Hfin; intros; subst. rewrite <- Nat2Z.inj_0 in H0. rewrite <- Nat2Z.inj_0 in H1. apply Nat2Z.inj in H0. apply Nat2Z.inj in H1. subst j k; exfalso; revert Hjk; apply Nat.lt_irrefl. 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