law nat_mod_lt

lawful-words@0.1.0.0 · LAWS.bend:473

import Base

473law nat_mod_lt:
474  for a: Nat
475  for b: Nat
476  for h: {Nat.is_lt(0n, b) == True{} : Bool}
477  {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}