def quotient_decode

stelliferous@0.0.2.0 · proofs/u32_division.bend:110

import Base

110def quotient_decode(pair: Word(32n) & U32) -> {U32.to_nat(U32.div.fin(pair)) == quotient(decode(32n,pair)) : Nat}:
111  (q,r) = pair
112  {==}