Definition abmonoidrer (X : abmonoid) (a b c d : X) : (a + b) + (c + d) = (a + c) + (b + d) := abmonoidoprer (pr2 X) a b c d.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.