proposition: Lemma fold_last : forall m f x l, Monoid m -> fold m f (l & x) = monoid_oper m (fold m f l) (f x).
proof: Proof. Proof using. intros. rewrite~ fold_app. rewrite fold_cons. rewrite fold_nil. rewrite monoid_neutral_r. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)