fact: Definition fold A B (m:monoid_op B) (f:A->B) (L:list A) : B := fold_right (fun x acc => monoid_oper m (f x) acc) (monoid_neutral m) L.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)