proposition: Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s}.
proof: Proof. exists (take (size s) m ++ nseq (size s - size m) false). by elim: s m => [|x s IHs] [|b m] //=; rewrite (size_nseq, IHs). by elim: s m => [|x s IHs] [|b m] //=; rewrite (mask_false, IHs). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)