proposition: Lemma find_umfilt k p f : find k (um_filter p f) = if find k f is Some v then if p (k, v) then Some v else None else None.
proof: Proof. elim/um_indf: f k=>[||k' v f IH W /(order_path_min (@trans K)) P] k. - by rewrite umfilt_undef find_undef. - by rewrite umfilt0 find0E. have W' : valid (pts k' v \+ um_filter p f). - rewrite validPtUn (validPtUn_cond W)valid_umfilt (validR W). by apply: contra (validPtUnD W)=>/dom_umfilt [x][_] /In_dom. rewrite umfiltPtUn W; case: ifP=>E; rewrite !findPtUn2 //; case: eqP=>// ->; rewrite E // IH. by move/validPtUnD: W; case: dom_find=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)