proposition: Theorem points_not_in_any_newton_segment₁ : ∀ pts ns, Sorted fst_lt pts → lower_convex_hull_points pts = Some ns → ∀ h αh, (h, αh) ∈ pts ∧ (h, αh) ∉ [ini_pt ns; fin_pt ns … oth_pts ns] → β ns < αh + h * γ ns.
proof: Proof. intros * Hsort Hnp h αh (Hh, Hnh). destruct ns as ((j, αj), (k, αk), segjk). remember cons as f in Hnh; simpl in Hnh; subst f. destruct (Qlt_le_dec k h) as [Hlt| Hge]. eapply lt_aft_k; simpl; eassumption. destruct (Qeq_dec h k) as [Heq| Hne]. eapply qeq_eq_fin in Heq; try eassumption. exfalso; revert Heq. eapply h_not_k; eassumption. destruct (Qlt_le_dec j h) as [Hlt| Hge₂]. apply Qle_neq_lt in Hge; [ idtac | assumption ]. eapply conj in Hge; [ idtac | eassumption ]. eapply lt_bet_j_and_k; eassumption. destruct (Qeq_dec h j) as [Heq| Hne₂]. eapply qeq_eq_ini in Heq; try eassumption. exfalso; revert Heq. eapply h_not_j; simpl; eassumption. apply Qle_neq_lt in Hge₂; [ idtac | assumption ]. eapply lt_bef_j; simpl; try eassumption. split; [ assumption | idtac ]. remember (mkns (j, αj) (k, αk) segjk) as ns. apply ini_lt_fin_pt with (ns := ns) in Hsort; [ | easy ]. subst ns; assumption. Qed.
imports: Utf8 QArith Sorting NPeano Misc Slope_base SlopeMisc ConvexHull ConvexHullMisc Newton NotInSegMisc