proposition: Lemma oex_ou V R (P : R -> Prop) a ks (h : natmap V) t (z0 : R) : uniq ks -> {in &=ks `]-oo, t[, oex_inv P a ks h z0} -> P z0 -> P (oexec_lt a ks t h z0).
proof: Proof. move=>U IH P0; apply: oev_indX=>// k ks1 ks2 v _ Kh Eh ->. have K : k \in &=ks `]-oo, t[ by rewrite Eh mem_cat inE eqxx orbT. have Nk : k \notin ks1. - move/(eqslice_uniq `]-oo, t[): U. by rewrite Eh cat_uniq /= negb_or -andbA; case/and5P. case/mem_uo: (K)=>// [Ks TK]. suff {IH U K}-> : ks1 = &=ks `]-oo, k[ by apply: IH. move: Eh; rewrite (eqslice_split (b:=true) (x:=k)) /=; last by rewrite lteBSide /= leEnat; apply: ltnW. rewrite eqsl_xoL TK => Eh; rewrite (cat_cancel _ _ Eh) //. by apply: eqsliceRO_notin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)