proposition: Lemma eqslice0 i : &=([::] : seq A) i = [::].
proof: Proof. by rewrite /eq_slice slice0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)