def DMOK

lawful-words@0.1.0.0 · proof_u32.bend:636

import Base

636# What U32.divmod.go(k, a, b) returns: q * b + r = a and r < b.
637def DMOK(k: Nat, A: Nat, B: Nat, qr: Word(k) & U32) -> Type:
638  match qr:
639    case (q, r):
640      Pair({Nat.add(Nat.mul(Word.to_nat(k, q), B), U32.to_nat(r)) == A : Nat}, {Nat.is_lt(U32.to_nat(r), B) == True{} : Bool})