proposition: Lemma slice_subset s i1 i2 : i1 <= i2 -> {subset (&:s i1) <= &:s i2}.
proof: Proof. case: i1=>i1 j1; case: i2=>i2 j2. rewrite subitvE; case/andP=>Hi Hj. move=>x Hx. have Hij : i1 <= j1. - apply: contraLR Hx; rewrite -ltNge=>/ltW Hji. by rewrite itv_swapped_bnd. rewrite (@slice_split_bnd _ _ _ i1) /=; last first. - by rewrite Hi /=; apply/le_trans/Hj. rewrite mem_cat; apply/orP; right. rewrite (@slice_split_bnd _ _ _ j1) /=; last first. - by rewrite Hj andbT. by rewrite mem_cat Hx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)