Definition isacommringapartdec ( R : acommring ) := isapartdec ( pr1 ( pr2 R ) ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.