proposition: Lemma fresh_mono A B (h1 : natmap A) (h2 : natmap B) : {subset dom h1 <= dom h2} -> fresh h1 <= fresh h2.
proof: Proof. by apply: lastkey_mono. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)