proposition: Theorem sorted_qeq_eq : ∀ pts j αj k αk, Sorted fst_lt pts → (j, αj) ∈ pts → (k, αk) ∈ pts → j == k → (j, αj) = (k, αk).
proof: Proof. intros pts j αj k αk Hsort Hj Hk Hjk. induction pts as [| (l, αl)]; [ contradiction | idtac ]. destruct Hj as [Hj| Hj]. destruct Hk as [Hk| Hk]. rewrite Hj in Hk; assumption. injection Hj; clear Hj; intros; subst l αl. clear IHpts. exfalso. induction pts as [| (l, αl)]; [ contradiction | idtac ]. destruct Hk as [Hk| Hk]. injection Hk; clear Hk; intros; subst l αl. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt, _). unfold fst_lt in Hlt; simpl in Hlt; rewrite Hjk in Hlt. apply Qlt_irrefl in Hlt; contradiction. apply IHpts; [ idtac | assumption ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. destruct Hk as [Hk| Hk]. injection Hk; clear Hk; intros; subst l αl. clear IHpts. exfalso. induction pts as [| (l, αl)]; [ contradiction | idtac ]. destruct Hj as [Hj| Hj]. injection Hj; clear Hj; intros; subst l αl. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt, _). unfold fst_lt in Hlt; simpl in Hlt; rewrite Hjk in Hlt. apply Qlt_irrefl in Hlt; contradiction. apply IHpts; [ idtac | assumption ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. apply Sorted_inv_1 in Hsort. apply IHpts; assumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc