proposition: Lemma dropEmask i s : drop i s = mask (nseq i false ++ nseq (size s - i) true) s.
proof: Proof. by elim: i s => [s|? ? []//]; rewrite drop0/= mask_true// subn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)