proposition: Lemma fold_eq_fold_list_repr : forall A B (m:monoid_op B) (f:A->B) (E: set A) L, Comm_monoid m -> list_repr E L -> fold m f E = LibList.fold m f L.
proof: Proof. Proof using. introv HM EL. rewrite fold_eq_fold_to_list. forwards~ (N&EQ2): eq_to_list_inv E. applys* finite_of_list_repr. destruct EL as (ND&EQ1). applys~ LibList.fold_equiv. intros. rewrite EQ2. rewrite* EQ1. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)