law div_block

bend-ml-llama@0.2.1.0 · main.bend:616

import Base

616# one block of 1 + m numbers in Nat.divmod: the counter m runs down to 0, then the quotient d grows by one
617law div_block:
618  for +m: Nat
619  for -n: Nat
620  for -d: Nat
621  for -r: Nat
622  {Nat.divmod.go(Nat.add(1n+m, n), m, d, r) == Nat.divmod.go(n, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}