law bump_go

stelliferous@0.0.2.0 · proofs/nat_division.bend:54

import Base

54law bump_go:
55  for +n: Nat
56  for +m: Nat
57  for +d: Nat
58  for +r: Nat
59  {Nat.divmod.go(n,m,1n+d,r) == bump(Nat.divmod.go(n,m,d,r)) : Nat & Nat}