proposition: Lemma eqsl_uL_consE s b k t : &=(k :: s) (Interval -oo (BSide b t)) = if t == k then if b then [::] else [::k] else k :: &=s (Interval -oo (BSide b t)).
proof: Proof. rewrite -cat1s eqsl_uL_catE /= inE; case: eqVneq=>// {t}->. by rewrite /eq_slice /= eqxx; case: b. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)