def small

stelliferous@0.0.2.0 · proofs/nat_division.bend:37

import Base
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

37def small(+r: Nat,+b: Nat,h: {Nat.is_lt(r,b) == True{} : Bool}) -> {Nat.divmod(r,b) == (0n,r) : Nat & Nat}:
38  match b:
39    case 0n:
40      Empty.absurd({Nat.divmod(r,0n) == (0n,r) : Nat & Nat},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(r,0n),True{},
41            Equal.sym(Bool,Nat.is_lt(r,0n),False{},lt_zero(r)),h)))
42    case 1n+ +p:
43      %Addition.zero_right(r) : {Nat.divmod.go(r,p,0n,0n) == (0n,_) : Nat & Nat}
44      go_small(r,p,0n,0n,lt_succ_le(r,p,h))