proposition: Lemma addb_seq_cat a b c d : size a = size c -> addb_seq (a ++ b) (c ++ d) = addb_seq a c ++ addb_seq b d.
proof: Proof. move=> a_c; by rewrite /addb_seq /= -map_cat zip_cat. Qed.
imports: mathcomp(all_ssreflect fingroup perm)