fact: Definition fold_impl (m:monoid_op B) (f:A->B) (E:set A) := LibList.fold_right (fun x acc => monoid_oper m (f x) acc) (monoid_neutral m) (to_list E).
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)