Definition natmultabmonoid : abmonoid := make_abmonoid (make_setwithbinop natset (λ n m : nat, n * m)) (make_dirprod (make_dirprod natmultassoc (@make_isunital natset _ 1 (make_dirprod natmultl1 natmultr1))) natmultcomm).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.