proposition: Theorem slope_expr_eq : ∀ pt₁ pt₂ pt₃ pts, Sorted fst_lt [pt₁; pt₂ … pts] → pt₃ ∈ pts → slope_expr pt₁ pt₂ == slope_expr pt₁ pt₃ → slope_expr pt₁ pt₂ == slope_expr pt₂ pt₃.
proof: Proof. intros pt₁ pt₂ pt₃ pts Hsort Hin H. apply slope_eq; [ idtac | idtac | idtac | assumption ]. intros HH. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt, _). unfold fst_lt in Hlt. rewrite HH in Hlt. apply Qlt_irrefl in Hlt; contradiction. intros HH. clear H. induction pts as [| pt₄]; [ contradiction | idtac ]. simpl in Hin. destruct Hin as [Hin| Hin]. subst pt₄. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₁, Hsort). apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₂, Hsort). unfold fst_lt in Hlt₂. rewrite HH in Hlt₂. apply Qlt_irrefl in Hlt₂; contradiction. apply IHpts; [ idtac | assumption ]. eapply Sorted_minus_3rd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. intros HH. clear H. induction pts as [| pt₄]; [ contradiction | idtac ]. simpl in Hin. destruct Hin as [Hin| Hin]. subst pt₄. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₁, Hsort). apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₂, Hsort). unfold fst_lt in Hlt₂. rewrite HH in Hlt₂. eapply Qlt_trans in Hlt₂; [ idtac | eassumption ]. apply Qlt_irrefl in Hlt₂; contradiction. apply IHpts; [ idtac | assumption ]. 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