proposition: Lemma exec0 a (h : natmap V) (z0 : R) : exec a 0 h z0 = z0.
proof: Proof. have /(eq_in_eval _) -> : forall kv, kv \In h -> le 0 kv = pred0 kv. - by case=>k v /In_cond; case: k. by rewrite eval_pred0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)