proposition: Lemma homo_sorted_in s : {in P &, {homo f : x y / e x y >-> e' x y}} -> all P s -> sorted e s -> sorted e' (map f s).
proof: Proof. by move=> f_mono; rewrite sorted_map; apply: sub_in_sorted. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)