proposition: Lemma umcntUn p f1 f2 : valid (f1 \+ f2) -> um_count p (f1 \+ f2) = um_count p f1 + um_count p f2.
proof: Proof. move=>W; rewrite /um_count umfiltUn // size_domUn //. by rewrite -umfiltUn // valid_umfilt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)