proposition: Lemma addb_seq_com : forall n a b, size a = n -> size b = n -> addb_seq a b = addb_seq b a.
proof: Proof. elim => [ [] // [] // | n IH [|ha ta] // [|hb tb] // ] [Ha] [Hb]. by rewrite /addb_seq /= -!/(addb_seq _ _) IH // addbC. Qed.
imports: mathcomp(all_ssreflect fingroup perm)