law mod_self

bend-mathlib@0.8.1.0 · nat.bend:1907

import Base

1907# A natural modulo itself is zero: n % n = 0.
1908law mod_self:
1909  for n: Nat
1910  {Nat.mod(n, n) == 0n : Nat}