proposition: Lemma rev_mask m s : size m = size s -> rev (mask m s) = mask (rev m) (rev s).
proof: Proof. move: m s; apply: seq_ind2 => //= b x m s eq_size_sm IH. by case: b; rewrite !rev_cons mask_rcons ?IH ?size_rev// (cats1, cats0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)