law nat_mod_small

lawful-words@0.1.0.0 · LAWS.bend:479

import Base

479law nat_mod_small:
480  for a: Nat
481  for b: Nat
482  for h: {Nat.is_lt(a, b) == True{} : Bool}
483  {Nat.mod(a, b) == a : Nat}