def div_mod

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32div.bend:196

import Base

196# THEOREM: div and mod are Euclidean division by any nonzero divisor.
197def div_mod(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))) == v(a) : Nat} & {Nat.is_lt(v(U32.mod(a, b)), v(b)) == True{} : Bool}:
198  match a b:
199    case U32{+aw} U32{+bw}:
200      dm_if(aw, U32{bw}, U32.is_zero(U32{bw}), hb, pos(U32{bw}, hb))