law mod_self_sym

bend-mathlib@0.8.1.0 · nat.bend:4383

import Base

4383# A natural modulo itself is zero: n % n = 0, reversed to rewrite toward the simple side.
4384law mod_self_sym:
4385  for n: Nat
4386  {0n == Nat.mod(n, n) : Nat}