NatDivision.bump_go: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_division.bend as NatDivision
Lines 54-59 of stelliferous@0.0.2.0/proofs/nat_division.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&start_line=54&end_line=59

import Base

law bump_go:
  for +n: Nat
  for +m: Nat
  for +d: Nat
  for +r: Nat
  {Nat.divmod.go(n,m,1n+d,r) == bump(Nat.divmod.go(n,m,d,r)) : Nat & Nat}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&name=bump