def div_block

bendtorch@1.3.0.0 · PROOF.bend:833

import Base
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

833# one block of 1 + m numbers adds 1 to the quotient (Nat.divmod.go counts down the remainder from m)
834def div_block(+m: Nat, -n: Nat, -d: Nat, -r: Nat) -> {Nat.divmod.go(Nat.add(1n+m, n), m, d, r) == Nat.divmod.go(n, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}:
835  match m:
836    case 0n:
837      {==}
838    case 1n+p:
839      %Equal.sym(Nat, 1n+Nat.add(p, r), Nat.add(p, 1n+r), NL.add_succ(p, r)) : {Nat.divmod.go(Nat.add(1n+p, n), p, d, 1n+r) == Nat.divmod.go(n, _, 1n+d, 0n) : Nat & Nat}
840      div_block(p, n, d, 1n+r)