proposition: Lemma mask_rcons b m x s : size m = size s -> mask (rcons m b) (rcons s x) = mask m s ++ nseq b x.
proof: Proof. by move=> ms; rewrite -!cats1 mask_cat//; case: b. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)