proposition: Theorem fold_symmetric : forall (A : Type) (f : A -> A -> A), (forall x y z : A, f x (f y z) = f (f x y) z) -> forall (a0 : A), (forall y : A, f a0 y = f y a0) -> forall (l : list A), fold_left f l a0 = fold_right f a0 l.
proof: Proof. intros A f assoc a0 comma0 l. induction l as [ | a1 l IHl]; [ simpl; reflexivity | ]. simpl. rewrite <- IHl. clear IHl. revert a1. induction l as [|? ? IHl]; [ auto | ]. simpl. intro. rewrite <- assoc. rewrite IHl. rewrite IHl. auto. Qed.
imports: PeanoNat