proposition: Theorem prod2list_app : forall l1 l2 l3 l4, length l1 = length l2 -> prod2list (l1 ++ l3) (l2 ++ l4) = prod2list l1 l2 + prod2list l3 l4.
proof: Proof. intros l1 l2 l3 l4 H; unfold prod2list in |- *. rewrite map2_app; auto. rewrite fold_left_app. rewrite Nat.add_comm. apply sym_equal. repeat rewrite fold_left_eta with (f := plus) (f1 := fun a b : nat => a + (fun x => x) b); auto. apply sym_equal; rewrite <- fold_plus_split with (f := fun x : nat => x); auto. apply Nat.add_comm. Qed.
imports: Coq(ArithRing Sorting.Permutation)