law cycle

stelliferous@0.0.2.0 · proofs/nat_division.bend:71

import Base

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