law div_blocks

bend-ml-llama@0.2.0.0 · main.bend:631

import Base

631# j whole blocks of 1 + s numbers add j to the quotient
632law div_blocks:
633  for +j: Nat
634  for +s: Nat
635  for +n: Nat
636  for +d: Nat
637  {Nat.divmod.go(Nat.add(Nat.mul(j, 1n+s), n), s, d, 0n) == Nat.divmod.go(n, s, Nat.add(j, d), 0n) : Nat & Nat}