fact: Definition um_mono_lt f := forall k k' v v', (k, v) \In f -> (k', v') \In f -> ord k k' -> ord v v'.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)