proposition: Lemma monoid_fold_symm: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (e: A) l, (forall x, f e x === x) -> (forall x, f x e === x) -> (forall x y z, f (f x y) z === f x (f y z)) -> fold_left f l e === fold_right f e l.
proof: Proof. intros. pose proof (proper_fold_left f). destruct l. + simpl. reflexivity. + simpl. rewrite H. revert a; induction l; intros; simpl. - symmetry; auto. - rewrite <- H1. apply IHl. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext Coq.Lists.List