fact: Definition um_foldr (a : K -> V -> R -> R) (z0 d : R) f := if valid f then foldr (fun kv z => a kv.1 kv.2 z) z0 (assocs f) else d.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)