proposition: Lemma slice_map {A B} (f : A -> B) i s : [seq f x | x <- &:s i] = &: [seq f x | x <- s] i.
proof: Proof. by rewrite !slice_mask /= map_mask /= size_map. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)