law nat_mod_lt

bend-osdev-u32@0.1.0.0 · LAWS_div.bend:13

import Base

13law nat_mod_lt:
14  for +a: Nat
15  for +bp: Nat
16  {Nat.is_lt(Nat.mod(a, 1n+bp), 1n+bp) == True{} : Bool}