proposition: Lemma fold_union : forall A B (m:monoid_op B) (f:A->B) (E F:set A), Comm_monoid m -> finite E -> finite F -> E \# F -> fold m f (E \u F) = monoid_oper m (fold m f E) (fold m f F).
proof: Proof. Proof using. introv HM HE HF HD. rewrites (>> fold_eq_fold_to_list E). rewrites (>> fold_eq_fold_to_list F). hint list_repr_to_list_of_finite. forwards~ HR: list_repr_disjoint_union HD. rewrites~ (>> fold_eq_fold_list_repr HR). rewrite~ LibList.fold_app. typeclass. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)