law mod_lt

bend-osdev-word64@0.1.1.0 · LAWS_div.bend:17

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

17law mod_lt:
18  for +a: W.W64
19  for +b: W.W64
20  for h: {W.W64.is_zero(b) == False{} : Bool}
21  {Nat.is_lt(W.W64.to_nat(W.W64.mod(a, b)), W.W64.to_nat(b)) == True{} : Bool}