Definition aintdom := ∑ A : acommring, ( ringunel2 ( X := A ) ) # 0 × forall a b : A, a # 0 -> b # 0 -> ( a * b ) # 0.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.