proposition: Lemma eqsl_rconsE s k b1 t1 b2 t2 : &=(rcons s k) (Interval (BSide b1 t1) (BSide b2 t2)) = if t1 \in s then if t2 \in s then &=s (Interval (BSide b1 t1) (BSide b2 t2)) else if b2 && (k==t2) then &=s (Interval (BSide b1 t1) +oo) else rcons (&=s (Interval (BSide b1 t1) +oo)) k else if t2 \in s then [::] else if [&& b1, k==t1 & (k==t2) ==> ~~b2] then [::k] else [::].
proof: Proof. rewrite -cats1 eqsl_catE. case/boolP: (t1 \in s)=>H1; case/boolP: (t2 \in s)=>H2 //. - rewrite /eq_slice /=; case: eqVneq; case B2: b2=>/= _; try by rewrite cats1. by rewrite cats0. by rewrite /eq_slice /=; case: eqVneq=>_; case: eqVneq=>_; case: b1; case: b2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)