proposition: Lemma drop_take_mask {A} (s : seq A) x y : drop x (take y s) = mask (nseq x false ++ nseq (y-x) true) s.
proof: Proof. case: (ltnP x (size s))=>Hx; last first. - rewrite drop_oversize; last by rewrite size_take_min geq_min Hx orbT. rewrite -{1}(subnKC Hx) nseqD -catA -{3}(cats0 s) mask_cat; last by rewrite size_nseq. by rewrite mask0 mask_false. have Hx': size (nseq x false) = size (take x s). - by rewrite size_nseq size_take_min; symmetry; apply/minn_idPl/ltnW. rewrite -{2}(cat_take_drop x s) mask_cat // mask_false /= -takeEmask take_drop. case: (leqP x y)=>[Hxy|/ltnW Hxy]; first by rewrite subnK. move: (Hxy); rewrite -subn_eq0=>/eqP->; rewrite add0n drop_take_id. by rewrite drop_oversize // size_take_min geq_min Hxy. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)