整数と言ってる時点で、加法・乗法・乗法逆元は定まってるし、>>617はおかしい。
除法は乗法逆元を掛けることで定義されるから。
おそらく、>>617はp 進数体とかの上での除法のこと言ってるんだろうけど。

整数の除法と言えば、>>616の定義しかない。

ただ、>>609で問題なのは負数に対するmoduloの定義。例えば、
-12 mod 5
が-2なのか3なのかは少し問題になるかもしれない。
普通は3なんだけど、順序の入ってない体での除法を考えた場合、
>>616の 0 ≦ r ＜ nの部分の定義が使えないから、

a mod b ⇔ a - b * xのうち最も0と"近い"もの

という定義も考えられる。距離または絶対値が入ってることが前提になるが。
この定義だと、-12 mod 5 = -2となる。