def mod_fin_ok

lawful-words@0.1.0.0 · proof_u32.bend:823

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

823def mod_fin_ok(+x: Nat, +y: Nat, qr: Word(32n) & U32, d: DMOK(32n, x, y, qr)) -> {U32.to_nat(U32.mod.fin(qr)) == Nat.mod(x, y) : Nat}:
824  match qr:
825    case (+q, +r):
826      match d:
827        case (+e1, +e2):
828          %e1 : {U32.to_nat(r) == Nat.mod(_, y) : Nat}
829          Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Word.to_nat(32n, q), y), U32.to_nat(r)), y), U32.to_nat(r), N.mod_mul_add(Word.to_nat(32n, q), y, U32.to_nat(r), e2))