proposition: Lemma mono_sorted_in s : {in P &, {mono f : x y / e x y >-> e' x y}} -> all P s -> sorted e' (map f s) = sorted e s.
proof: Proof. by case: s => // x s; apply: mono_path_in. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)