def step_bound

stelliferous@0.0.2.0 · proofs/binary_division.bend:110

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

110def step_bound(+bit: Bool,+b: Nat,+prev: Quotient,h: {Nat.is_lt(remainder(prev),b) == True{} : Bool}) -> {Nat.is_lt(remainder(step(bit,b,prev)),
111    b) == True{} : Bool}:
112  Quotient{+q,+r} = prev
113  branch_bound(Nat.is_ge(Comparison.digit(bit,r),b),Nat.double(q),Comparison.digit(bit,r),b,{==},Order.digit_lt(r,b,bit,h))