~/jendhub

def natural_quotient

stelliferous@0.0.2.0 · proofs/u32_division.bend:126

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

126def natural_quotient(+w: Word(32n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.div(Word.to_nat(32n,w),
127    b) == quotient(BinaryDivision.go(32n,w,b)) : Nat}:
128  %Equal.sym(Nat & Nat,Nat.divmod(Word.to_nat(32n,w),b),BinaryDivision.pair(BinaryDivision.go(32n,w,b)),BinaryDivision.natural(32n,w,b,
129      positive)) : {Pair.fst(Nat,Nat,_) == quotient(BinaryDivision.go(32n,w,b)) : Nat}
130  quotient_pair(BinaryDivision.go(32n,w,b))

Uses (15)

Used by (1)