proposition: Lemma fold_app : forall m f l1 l2, Monoid m -> fold m f (l1 ++ l2) = monoid_oper m (fold m f l1) (fold m f l2).
proof: Proof. Proof using. unfold fold. intros. rewrite fold_right_app. gen l2. induction l1; intros. repeat rewrite fold_right_nil. rewrite~ monoid_neutral_l. repeat rewrite fold_right_cons. rewrite <- monoid_assoc. fequals. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)