This file defines the basics of the divisibility relation in the context of
Main definitions #
Implementation notes #
The divisibility relation is defined for all monoids, and as such, depends on the order of
multiplication if the monoid is not commutative. There are two possible conventions for
divisibility in the noncommutative context, and this relation follows the convention for ordinals,
a | b is defined as
∃ c, b = a * c.