Definition ringpossubmonoid (X : ring) {R : hrel X} (is1 : isringmultgt X R) (is2 : R 1 0) : @submonoid (ringmultmonoid X). Proof. intros. exists (λ x, R x 0). split. - intros x1 x2. apply is1. apply (pr2 x1). apply (pr2 x2). - apply is2. Defined.
Require Import UniMath.Algebra.Groups.