~/jendhub

def dm_e2

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64div.bend:28

import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as U64div
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD

28def dm_e2(+a: U32, +b: U32, h: UD.dm_type(a, b)) -> {Nat.add(Nat.mul(UD.v(U32.div(a, b)), UD.v(b)), UD.v(U32.mod(a, b))) == UD.v(a) : Nat}:
29  (e, l) = h
30  e

Uses (9)

Used by (1)