proposition: Lemma mask_true s n : size s <= n -> mask (nseq n true) s = s.
proof: Proof. by elim: s n => [|x s IHs] [|n] //= Hn; congr (_ :: _); apply: IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)