proposition: Lemma umfilt_pleqI x p : [pcm um_filter p x <= x].
proof: Proof. exists (um_filter (predD predT p) x); rewrite -umfilt_predU. by rewrite -{1}[x]umfilt_predT; apply/eq_in_umfilt=>a; rewrite /= orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)