def transfer_bound

stelliferous@0.0.2.0 · proofs/u32_division.bend:79

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

79def transfer_bound(+prev: BinaryDivision.Quotient,+next: BinaryDivision.Quotient,+b: Nat,e: {prev == next : BinaryDivision.Quotient},
80  h: {Nat.is_lt(BinaryDivision.remainder(next),b) == True{} : Bool}) -> {Nat.is_lt(BinaryDivision.remainder(prev),b) == True{} : Bool}:
81  %Equal.sym(BinaryDivision.Quotient,prev,next,e) : {Nat.is_lt(BinaryDivision.remainder(_),b) == True{} : Bool}
82  h