def internal_dm_inv

bend-mathlib@0.8.1.0 · u32.bend:852

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

852def internal_dm_inv(m: Nat, b: Nat, a: Nat, qr: Word(m) & U32) -> Type:
853  match qr:
854    case (q, r):
855      {Nat.add(Nat.mul(Word.to_nat(m, q), b), U32.to_nat(r)) == a : Nat} & MNat.lt(U32.to_nat(r), b)