def div_fin_ok

lawful-words@0.1.0.0 · proof_u32.bend:815

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

815def div_fin_ok(+x: Nat, +y: Nat, qr: Word(32n) & U32, d: DMOK(32n, x, y, qr)) -> {U32.to_nat(U32.div.fin(qr)) == Nat.div(x, y) : Nat}:
816  match qr:
817    case (+q, +r):
818      match d:
819        case (+e1, +e2):
820          %e1 : {Word.to_nat(32n, q) == Nat.div(_, y) : Nat}
821          Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(Word.to_nat(32n, q), y), U32.to_nat(r)), y), Word.to_nat(32n, q), N.div_mul_add(Word.to_nat(32n, q), y, U32.to_nat(r), e2))