fact: Definition slice {A : Type} (s : seq A) (i : interval nat) := let sz := size s in let: Interval l u := i in drop (bnd l sz) (take (bnd u sz) s).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)