def split

bend-collections-laws-math@1.0.0.0 · proofs/math/number/egcd.bend:86

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

86# a == (a div b) b + a mod b
87def split(+a: Nat, +bp: Nat) -> {a == Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) : Nat}:
88  R.dm_eq(bp, a)