proposition: Lemma slice_sorted r s i : sorted r s -> sorted r (&:s i).
proof: Proof. move=>S; rewrite /slice /=; case: i=>l u. by apply/drop_sorted/take_sorted. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)