law mod_one

bend-mathlib@0.8.1.0 · nat.bend:1890

import Base

1890# Any natural modulo one is zero: a % 1 = 0.
1891law mod_one:
1892  for a: Nat
1893  {Nat.mod(a, 1n) == 0n : Nat}