fact: Definition int_abs `{ia : IntAbs} (x : Z) : N := match int_abs_sig x with | inl (n↾_) => n | inr (n↾_) => n end.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories MathClasses.categories.varieties