proposition: Theorem Sorted_trans_app : ∀ A (g : A → A → Prop) x y l, (∀ x y z, g x y → g y z → g x z) → x ∈ l → Sorted g (l ++ [y]) → g x y.
proof: Proof. intros A g x y l Htrans Hx Hsort. apply Sorted_LocallySorted_iff in Hsort. revert x y Hx Hsort. induction l as [| z]; intros; [ contradiction | idtac ]. simpl in Hsort. inversion Hsort. symmetry in H1. apply List.app_eq_nil in H1. destruct H1 as (_, H); discriminate H. subst. destruct Hx as [Hx| Hx]. subst z. destruct l as [| z]. simpl in H0. injection H0; clear H0; intros; subst. assumption. eapply Htrans; [ eassumption | idtac ]. apply IHl. simpl in H0. injection H0; clear H0; intros; subst. left; reflexivity. rewrite <- H0; assumption. apply IHl; [ assumption | idtac ]. rewrite <- H0; assumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base