proposition: Lemma itv_swapped_bnd s (i j : itv_bound nat) : j <= i -> &:s (Interval i j) = [::].
proof: Proof. move=>H; rewrite /slice; apply: drop_oversize. move: H; case: i=>[ib ix|[]]; case: j=>[jb jx|[]] //=; rewrite ?bnd_simp ?take_size ?take0 ?drop_size //= size_take_min. - rewrite leBSide; case: ib=>/=; case: jb=>/=; rewrite ?addn0 ?addn1=>Hji. - apply/leq_trans/Hji; exact: geq_minl. - apply/leq_trans/Hji; exact: geq_minl. - apply: leq_trans; first by exact: geq_minl. by apply: ltnW. by apply: leq_trans; first by exact: geq_minl. by move=>_; exact: geq_minr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)