proposition: Lemma slice_mask s i : &:s i = let x := bnd i.1 (size s) in let y := bnd i.2 (size s) in mask (nseq x false ++ nseq (y-x) true) s.
proof: Proof. by rewrite /slice /=; case: i=>i j /=; rewrite drop_take_mask. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)