def div_le

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/arith.bend:121

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

121# a quotient never exceeds its dividend
122def div_le(+a: Nat, +d: Nat) -> {Nat.is_le(Nat.div(a, d), a) == True{} : Bool}:
123  match d:
124    case 0n:
125      N.zero_le(a)
126    case 1n+bp:
127      go_le(a, bp, 0n, 0n)