proposition: Lemma eqsl_uR_consE s b k t : &=(k :: s) (Interval (BSide b t) +oo) = if t == k then if b then k::s else s else &=s (Interval (BSide b t) +oo).
proof: Proof. rewrite -cat1s eqsl_uR_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)