Abstract
We formalise key concepts and axioms of the divisibility relation on natural numbers using relation algebras. They use standard relational constructions for extrema, bounds, suprema, the univalent part and symmetric quotients, which we also formalise. We moreover prove that mono-atomic elements correspond to join-irreducible elements under the divisibility axioms.