proposition: Theorem minimise_slope_expr_le : ∀ pt₁ pt₂ pt₃ pts ms, Sorted fst_lt [pt₁; pt₂ … pts] → minimise_slope pt₁ pt₂ pts = ms → fin_pt ms = pt₃ → fst pt₂ < fst pt₃ → slope_expr pt₂ pt₃ <= slope ms.
proof: Proof. intros pt₁ pt₂ pt₃ pts ms Hsort Hms Hend Hlt. rewrite slope_slope_expr; [ idtac | eassumption ]. revert pt₁ pt₂ pt₃ ms Hsort Hms Hend Hlt. induction pts as [| pt₄]; intros. subst pt₃ ms; apply Qlt_irrefl in Hlt; contradiction. 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 |- *. apply Qeq_alt in Heqc. symmetry in Hend. remember Heqms₁ as H; clear HeqH. eapply minimised_slope in Heqms₁; [ idtac | eassumption ]. rewrite slope_slope_expr in Heqms₁; [ idtac | eassumption ]. rewrite <- Heqc in Heqms₁ |- *. eapply slope_expr_eq in Heqms₁; try eassumption. rewrite Heqms₁; apply Qle_refl. rewrite Hend. eapply end_pt_in; eassumption. subst ms; simpl in Hend |- *. subst pt₃. apply Sorted_inv_2 in Hsort; destruct Hsort as (_, Hsort). apply Sorted_inv_2 in Hsort; destruct Hsort as (H, _). apply Qlt_irrefl in Hlt; contradiction. move Hms at top; subst ms₁. apply Qgt_alt in Heqc. clear IHpts. revert pt₁ pt₂ pt₃ pt₄ ms Hsort Hend Hlt Heqms₁ Heqc. induction pts as [| pt₅]; intros. simpl in Heqms₁. subst ms; simpl. simpl in Hend, Heqc. subst pt₄. apply Qlt_le_weak. apply slope_lt_1312_2313; [ idtac | assumption ]. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₁, Hsort). apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₂, Hsort). split; assumption. simpl in Heqms₁. remember (minimise_slope pt₁ pt₅ pts) as ms₂. symmetry in Heqms₂. remember (slope_expr pt₁ pt₄ ?= slope ms₂) as c₁. symmetry in Heqc₁. destruct c₁. subst ms; simpl in Hend, Heqc |- *. eapply IHpts; try eassumption. eapply Sorted_minus_3rd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. subst ms; simpl in Hend, Heqc |- *. subst pt₄. apply Qlt_le_weak. apply slope_lt_1312_2313; [ idtac | assumption ]. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₁, Hsort). apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₂, Hsort). split; assumption. subst ms; simpl in Hend |- *. eapply IHpts; try eassumption. eapply Sorted_minus_3rd; [ 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