law mod_one

lawful-words@0.1.0.0 · proof_nat.bend:1137

import Base

1137law mod_one:
1138  for +a: Nat
1139  {Nat.mod(a, 1n) == 0n : Nat}