Definition rigaddsubmonoid {X : rig} : subrig X → @subabmonoid (rigaddabmonoid X) := λ A, @make_submonoid (rigaddabmonoid X) (pr1 A) (pr1 (pr2 A)).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.