proposition: Lemma mem_mask_rot m s : size m = size s -> mask (rot n0 m) (rot n0 s) =i mask m s.
proof: Proof. by move=> Ems x; rewrite mask_rot // mem_rot. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)