def finish

stelliferous@0.0.2.0 · proofs/binary_division.bend:145

import Base
import stelliferous@0.0.2.0/proofs/nat_division.bend as Division

145def finish(+a: Nat,+b: Nat,+result: Quotient,e: {total(result,b) == a : Nat},positive: {Nat.is_lt(0n,b) == True{} : Bool},
146  bounded: {Nat.is_lt(remainder(result),b) == True{} : Bool}) -> {Nat.divmod(a,b) == pair(result) : Nat & Nat}:
147  Quotient{+q,+r} = result
148  Division.unique(a,b,q,r,Equal.sym(Nat,Nat.add(Nat.mul(q,b),r),a,e),positive,bounded)