Formalizing symmetric remainder division (related to balanced modulo) – feedback on definitions & boundaries appreciated