proposition: Lemma eqsl_uo_split t (s1 s2 : seq A) : t \notin s1 -> &=(s1++t::s2) `]-oo, t[ = s1.
proof: Proof. by move=>X1; rewrite eqsl_uL_catE (negbTE X1) eqsl_uL_consE eqxx cats0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)