def remainder_pair

stelliferous@0.0.2.0 · proofs/u32_division.bend:122

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

122def remainder_pair(+result: BinaryDivision.Quotient) -> {Pair.snd(Nat,Nat,BinaryDivision.pair(result)) == BinaryDivision.remainder(result) : Nat}:
123  BinaryDivision.Quotient{q,r} = result
124  {==}