Definition natcommrig : commrig. Proof. split with (make_setwith2binop natset (make_dirprod (λ n m : nat, n + m) (λ n m : nat, n * m))). split. - split. + split with (make_dirprod (make_dirprod (make_dirprod natplusassoc (@make_isunital natset _ 0 (make_dirprod natplusl0 natplusr0))) natpluscomm) (make_dirprod natmultassoc (@make_isunital natset _ 1 (make_dirprod natmultl1 natmultr1)))). apply (make_dirprod natmult0n natmultn0). + apply (make_dirprod natldistr natrdistr). - unfold iscomm. apply natmultcomm. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.