proposition: Theorem j_lt_k : ∀ (f : puis_ser_pol α) j k L, newton_segments f = Some L → j = nat_num (fst (ini_pt L)) → k = nat_num (fst (fin_pt L)) → (j < k)%nat.
proof: Proof. intros f j k L HL Hj Hk. unfold newton_segments in HL. remember (points_of_ps_polynom f) as pts. remember Heqpts as Hj₁; clear HeqHj₁; symmetry in Hj₁. eapply pt_absc_is_nat with (pt := ini_pt L) in Hj₁. remember Heqpts as Hk₁; clear HeqHk₁; symmetry in Hk₁. eapply pt_absc_is_nat with (pt := fin_pt L) in Hk₁. apply points_of_polyn_sorted in Heqpts. assert (fst (ini_pt L) < fst (fin_pt L)). eapply ini_lt_fin_pt; eassumption. rewrite Hj₁, Hk₁ in H. apply Qnat_lt in H. subst j k; assumption. apply ini_fin_ns_in_init_pts; assumption. apply ini_fin_ns_in_init_pts; assumption. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base