law div_blocks

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

import Base

632# j whole blocks of 1 + s numbers add j to the quotient
633law div_blocks:
634  for +j: Nat
635  for +s: Nat
636  for +n: Nat
637  for +d: Nat
638  {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}