proposition: Theorem j_lt_h : ∀ (f : puis_ser_pol α) j αj jq h αh hq L, newton_segments f = Some L → (jq, αj) = ini_pt L → (hq, αh) ∈ oth_pts L → jq = Qnat j → hq = Qnat h → (j < h)%nat.
proof: Proof. intros f j αj jq h αh hq L HL Hj Hh Hjq Hhq. eapply jq_lt_hq in Hh; try eassumption. rewrite Hjq, Hhq in Hh. apply Qnat_lt; 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