proposition: Theorem prod2list_eq : forall a b c l1 l2 l3 l4 l5 l6, length l1 = length l4 -> length l2 = length l5 -> length l3 = length l6 -> prod2list (l1 ++ a :: l2 ++ a :: l3) (l4 ++ b :: l5 ++ c :: l6) = prod2list (l1 ++ a :: l2 ++ a :: l3) (l4 ++ c :: l5 ++ b :: l6).
proof: Proof. intros a b c l1 l2 l3 l4 l5 l6 H H0 H1; change (prod2list (l1 ++ (a :: []) ++ l2 ++ (a :: []) ++ l3) (l4 ++ (b :: []) ++ l5 ++ (c :: []) ++ l6) = prod2list (l1 ++ (a :: []) ++ l2 ++ (a :: []) ++ l3) (l4 ++ (c :: []) ++ l5 ++ (b :: []) ++ l6)) in |- *. repeat rewrite prod2list_app; auto with arith. ring. Qed.
imports: Coq(ArithRing Sorting.Permutation)