proposition: Lemma eqslice_sorted r s i : sorted r s -> sorted r (&=s i).
proof: Proof. by exact: slice_sorted. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)