fact: Definition growing (h : natmap V) := forall k v z0, (k, v) \In h -> oleq (f z0) (f (a z0 v)).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)