Definition make_ideal (S : subabmonoid (rigaddabmonoid R)) (isl : is_lideal S) (isr : is_rideal S) : ideal := tpair _ S (make_dirprod isl isr).
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.