proposition: Lemma oexlt_oexle_last V R a k ks t (h : natmap V) (z0 : R) : uniq (k::ks) -> t != k -> oexec_lt a (k::ks) t h z0 = oexec_le a (k::ks) (last k (&=ks `]-oo, t[)) h z0.
proof: Proof. move=>U Ntk; rewrite /oexec_lt/oexec_le [LHS]oevFK [RHS]oevFK. by rewrite eqsl_uox_last. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)