proposition: Lemma umfilt_pleq_mono x y (p : pred (K * V)) : [pcm x <= y] -> [pcm um_filter p x <= um_filter p y].
proof: Proof. move=>H; case W : (valid y). - by case: H W=>a -> W; rewrite umfiltUn //; eexists _. by move/invalidE: (negbT W)=>->; rewrite umfilt_undef; apply: umpleq_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)