proposition: Lemma mem_shl n m i : (n \in shl_itv i m) = (m + n \in i).
proof: Proof. rewrite !in_itv; case: i=>i j /=. case: i=>[l i|[]]; case: j=>[r j|[]] //=; rewrite ?andbF ?andbT //. - case: (ltnP j m)=>/= Hj. - rewrite andbF; symmetry; apply/negbTE; rewrite negb_and lteifNE negbK -lteifNE. by apply/orP; right; apply/lteifS/ltn_addr. have ->: (n < j - m ?<= if ~~ r) = (m + n < j ?<= if ~~ r). - case: r=>/=; first by rewrite ltEnat /= ltn_subRL. by rewrite leEnat leq_subRL. case: (m + n < j ?<= if ~~ r); rewrite ?andbF // !andbT. case: (ltnP i m)=>/= Hi. - by symmetry; apply/lteifS/ltn_addr. case: l=>/=; last by rewrite ltEnat /= ltn_subLR. by rewrite leEnat leq_subLR. - case: (ltnP i m)=>/= Hi. - by symmetry; apply/lteifS/ltn_addr. case: l=>/=; last by rewrite ltEnat /= ltn_subLR. by rewrite leEnat leq_subLR. case: (ltnP j m)=>/= Hj. - symmetry; apply/negbTE; rewrite lteifNE negbK. by apply/lteifS/ltn_addr. case: r=>/=; first by rewrite ltEnat /= ltn_subRL. by rewrite leEnat leq_subRL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)