proposition: Lemma oexlt_split V R a x1 t1 t2 x2 (h : natmap V) (z0 : R) : uniq (x1++t1::t2::x2) -> oexec_lt a (x1++t1::t2::x2) t2 h z0 = oexec_le a (x1++t1::t2::x2) t1 h z0.
proof: Proof. move=>U; apply: oexlt_consec=>//; apply/consecP_split=>//. - by rewrite mem_cat !inE eqxx !orbT. by exists x1, x2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)