proposition: Lemma umcnt_leq p1 p2 f : subpred p1 p2 -> um_count p1 f <= um_count p2 f.
proof: Proof. move=>S; case W: (valid f); last first. - by move/negbT/invalidE: W=>->; rewrite !umcnt_undef. rewrite /um_count (umfilt_predD _ S) size_domUn ?leq_addr //. by rewrite -umfilt_predD // valid_umfilt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)