law div_rest

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

import Base

651# fewer than 1 + s numbers after the last whole block leave the quotient alone
652law div_rest:
653  for +i: Nat
654  for -k: Nat
655  for -d: Nat
656  for -r: Nat
657  {Pair.fst(Nat, Nat, Nat.divmod.go(i, Nat.add(i, k), d, r)) == d : Nat}