proposition: Lemma fold_empty : forall A B (m:monoid_op B) (f:A->B), fold m f (\{}:set A) = monoid_neutral m.
proof: Proof. Proof using. intros. rewrite fold_eq_fold_to_list. rewrite to_list_empty. rewrite~ LibList.fold_nil. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)