Definition iscancelableif {X : hSet} (opp : binop X) (x : X) (isl : ∏ a b : X, opp x a = opp x b → a = b) (isr : ∏ a b : X, opp a x = opp b x → a = b) : iscancelable opp x := islcancelableif opp x isl ,, isrcancelableif opp x isr.
Require Import UniMath.Algebra.Groups.