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