proposition: Theorem min_slope_le : ∀ pt₁ pt₂ pt₃ pt₄ pts ms, Sorted fst_lt [pt₁; pt₂ … pts] → minimise_slope pt₁ pt₂ pts = ms → pt₃ ∈ pts → fin_pt ms = pt₄ → fst pt₃ < fst pt₄ → slope_expr pt₃ pt₄ <= slope ms.
proof: Proof. intros pt₁ pt₂ pt₃ pt₄ pts ms Hsort Hms Hpt Hend Hlt. rewrite slope_slope_expr; [ idtac | eassumption ]. revert pt₁ pt₂ pt₃ pt₄ ms Hsort Hms Hpt Hend Hlt. induction pts as [| pt₅]; [ contradiction | intros ]. simpl in Hms. remember (minimise_slope pt₁ pt₅ pts) as ms₁. symmetry in Heqms₁. remember (slope_expr pt₁ pt₂ ?= slope ms₁) as c. symmetry in Heqc. rewrite slope_slope_expr in Heqc; [ idtac | eassumption ]. destruct c. subst ms; simpl in Hend |- *. destruct Hpt as [Hpt| Hpt]. subst pt₅. rewrite <- slope_slope_expr; [ idtac | eassumption ]. eapply minimise_slope_expr_le; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. eapply IHpts; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. subst ms; simpl in Hend |- *; subst pt₄. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₁, Hsort). apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₂, Hsort). eapply Qlt_trans in Hlt₂; [ idtac | eassumption ]. exfalso; revert Hpt. eapply Sorted_not_in; [ idtac | idtac | eassumption | eassumption ]. intros x H; apply Qlt_irrefl in H; contradiction. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. move Hms at top; subst ms₁. destruct Hpt as [Hpt| Hpt]. subst pt₅. rewrite <- slope_slope_expr; [ idtac | eassumption ]. eapply minimise_slope_expr_le; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. eapply IHpts; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. Qed.
imports: Utf8 QArith Sorting NPeano Misc Slope_base SlopeMisc ConvexHull ConvexHullMisc Newton NotInSegMisc