def ud.div_mod

bend-osdev-u32@0.1.0.0 · PROOF_div.bend:94

import bend-osdev-u32@0.1.0.0/PROOF_div.bend as PROOFDiv

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

94def ud.div_mod(+k: Nat, +bp: Nat) -> {Nat.add(Nat.mul(Nat.div(k, 1n+bp), 1n+bp), Nat.mod(k, 1n+bp)) == k : Nat}:
95  Equal.trans(Nat, ud.dm_lhs(k, bp, 0n, 0n, bp), Nat.add(k, 0n), k, ud.dm_sum(k, bp, 0n, 0n, bp, UL.nat_add_zero(bp)), UL.nat_add_zero(k))

Uses (9)

Used by (2)