proposition: Lemma eqsl_swapped s (i j : itv_bound A) : bnd (ix_bnd s j) (size s) <= bnd (ix_bnd s i) (size s) -> &=s (Interval i j) = [::].
proof: Proof. by move=>H; rewrite /eq_slice /=; apply: itv_swapped. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)