proposition: Theorem jz_lt_kz : ∀ (f : puis_ser_pol α) jz kz L, newton_segments f = Some L → jz = Qnum (fst (ini_pt L)) → kz = Qnum (fst (fin_pt L)) → (jz < kz)%Z.
proof: Proof. intros f jz kz L HL Hjz Hkz. remember HL as H; clear HeqH. eapply j_lt_k in H; try reflexivity. remember (ini_pt L) as jaj. destruct jaj as (j, aj). remember (fin_pt L) as kak. destruct kak as (k, ak). simpl in Hjz, Hkz, H. subst jz kz. unfold nat_num in HL. apply Z2Nat.inj_lt; [ idtac | idtac | assumption ]. unfold newton_segments in HL. remember (points_of_ps_polynom f) as pts. symmetry in Heqpts. remember Heqpts as Hpts; clear HeqHpts. apply pt_absc_is_nat with (pt := (j, aj)) in Hpts. simpl in Hpts; rewrite Hpts. apply Zle_0_nat. rewrite Heqjaj. apply ini_fin_ns_in_init_pts; assumption. unfold newton_segments in HL. remember (points_of_ps_polynom f) as pts. symmetry in Heqpts. remember Heqpts as Hpts; clear HeqHpts. apply pt_absc_is_nat with (pt := (k, ak)) in Hpts. simpl in Hpts; rewrite Hpts. apply Zle_0_nat. rewrite Heqkak. 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