law u32_mod_lt

bend-osdev-u32@0.1.0.0 · LAWS.bend:506

import Base

506law u32_mod_lt:
507  for +a: U32
508  for +b: U32
509  for h: {U32.is_zero(b) == False{} : Bool}
510  {Nat.is_lt(U32.to_nat(U32.mod(a, b)), U32.to_nat(b)) == True{} : Bool}