proposition: Theorem Sorted_map : ∀ A B P (Q : A → B) (l : list A), Sorted (λ x y, P (Q x) (Q y)) l → Sorted P (List.map Q l).
proof: Proof. intros A B P Q l Hsort. apply Sorted_LocallySorted_iff in Hsort. apply Sorted_LocallySorted_iff. induction l as [| a]; [ constructor | simpl ]. destruct l as [| b]; simpl; constructor. apply IHl. inversion Hsort; subst; assumption. inversion Hsort; subst; assumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base