Require Import monoid.
Require Import Mult.

Lemma standard : monoid nat.
refine (mkmonoid nat 1 mult _ _ _); auto with arith.
Defined.