NatDivision.cycle: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_division.bend as NatDivision
Lines 71-76 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=71&end_line=76

import Base

law cycle:
  for +m: Nat
  for +tail: Nat
  for +d: Nat
  for +r: Nat
  {Nat.divmod.go(Nat.add(1n+m,tail),m,d,r) == Nat.divmod.go(tail,Nat.add(m,r),1n+d,0n) : Nat & Nat}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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/natural_addition.bend&name=successor_right