proposition: Lemma sorted_filter k s : sorted ord (map key s) -> sorted ord (map key (filter (predCk k) s)).
proof: Proof. by move=>H; rewrite -filter_map sorted_filter //; apply: trans. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)