Definition isbinopapartr { X : hSet } ( R : apart X ) ( opp : binop X ) := forall a b c : X, pr1 R ( opp b a ) ( opp c a ) -> pr1 R b c.
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.