proposition: Lemma sorted_kfilter (p : pred K) s : sorted ord (map key (kfilter' p s)).
proof: Proof. by case: s=>s H; rewrite -filter_map path.sorted_filter //; apply: trans. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)