proposition: Theorem Sorted_app_at_r : ∀ α f l (x : α), Sorted f l → (∀ y, y ∈ l → f y x) → Sorted f (l ++ [x]).
proof: Proof. clear; intros α f l x Hs Hf. induction l as [| z]; [ constructor; constructor | simpl ]. apply Sorted_inv in Hs. destruct Hs as (Hs, Hr). apply IHl in Hs. constructor; [ assumption | idtac ]. destruct l as [| t]. constructor; apply Hf; left; reflexivity. constructor; apply HdRel_inv in Hr; assumption. intros y Hy. apply Hf; right; assumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base