Number.ResidueClass.Maybe

Here we try to provide implementations for zero and one by making the modulus optional. We have to provide non-modulus operations for the cases where both operands have Nothing modulus. This is problematic since operations like (\/) depend essentially on the modulus.

A working version with disabled zero and one can be found ResidueClass.

r /: m is the residue class containing r with respect to the modulus m

Check if two residue classes share the same modulus