proposition: Lemma eqsl_uL_rconsE s b k t : &=(rcons s k) (Interval -oo (BSide b t)) = if t \in s then &=s (Interval -oo (BSide b t)) else if ~~ b || (t!=k) then rcons s k else s.
proof: Proof. rewrite -cats1 eqsl_uL_catE /=; case: ifP=>//= _. by rewrite eqsl1_uL; case: ifP=>_ //; rewrite cats0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)