Definition nataddabmonoid : abmonoid := make_abmonoid (make_setwithbinop natset (λ n m : nat, n + m)) (make_dirprod (make_dirprod natplusassoc (@make_isunital natset _ 0 (make_dirprod natplusl0 natplusr0))) natpluscomm).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.