proposition: Theorem Sorted_app {A} : ∀ (f : A → A → Prop) l₁ l₂, Sorted f (l₁ ++ l₂) → Sorted f l₁ ∧ Sorted f l₂.
proof: Proof. intros f l₁ l₂ H. split. induction l₁ as [| x]; [ constructor | simpl in H ]. destruct l₁ as [| y]; [ constructor; constructor | idtac ]. constructor; [ eapply IHl₁, Sorted_inv_1; eassumption | idtac ]. constructor; apply Sorted_inv_2 in H; destruct H; assumption. induction l₁ as [| x]; [ assumption | apply IHl₁ ]. eapply Sorted_inv_1; eassumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base