proposition: Lemma mono_sorted : {mono f : x y / e x y >-> e' x y} -> {mono map f : s / sorted e s >-> sorted e' s}.
proof: Proof. by move=> f_mon [] //= x s; apply: mono_path. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)