proposition: Lemma addb_seq_map A : forall n (a b : seq A) f, size a = n -> size b = n -> addb_seq (map f a) (map f b) = map (fun x => f x.1 (+) f x.2) (zip a b).
proof: Proof. elim => [[] // [] //| n IH [|ha ta] // [|hb tb] //= f [Ha] [Hb]]. by rewrite /addb_seq /= -IH. Qed.
imports: mathcomp(all_ssreflect fingroup perm)