proposition: Lemma eval_le0 A R a (h : natmap A) (z0 : R) : eval a (le 0) h z0 = z0.
proof: Proof. case W : (valid h); last first. - by move/negbT/invalidE: W=>->; rewrite eval_undef. rewrite eval_umfilt umfilt_mem0L ?eval0 //. by move=>k v /In_dom/dom_cond; rewrite /=; case: ltngtP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)