def remainder_decode

stelliferous@0.0.2.0 · proofs/u32_division.bend:114

import Base
import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision

114def remainder_decode(pair: Word(32n) & U32) -> {U32.to_nat(U32.mod.fin(pair)) == BinaryDivision.remainder(decode(32n,pair)) : Nat}:
115  (q,r) = pair
116  {==}