proposition: Lemma mask_rot m s : size m = size s -> mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s).
proof: Proof. move=> Ems; rewrite mask_cat ?size_drop ?Ems // -rot_size_cat. by rewrite size_mask -?mask_cat ?size_take ?Ems // !cat_take_drop. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)