proposition: Theorem exists_fin_pt_nat_fst_seg : ∀ f L, L = option_get phony_ns (newton_segments f) → ∃ i αi, fin_pt L = (Qnat i, αi).
proof: Proof. intros f L HL. remember (newton_segments f) as Ll eqn:HLl . symmetry in HLl. destruct Ll as [L₁| ]. simpl in HL; subst L₁. now eapply exists_fin_pt_nat with (f := f). subst L; simpl. exists 0%nat, 0; reflexivity. 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