def quotient_pair

stelliferous@0.0.2.0 · proofs/u32_division.bend:118

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

118def quotient_pair(+result: BinaryDivision.Quotient) -> {Pair.fst(Nat,Nat,BinaryDivision.pair(result)) == quotient(result) : Nat}:
119  BinaryDivision.Quotient{q,r} = result
120  {==}