def drain

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:116

import Base
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

116def drain(+k: Nat, -n: Nat, -m: Nat, -d: Nat, +r: Nat) -> {Nat.divmod.go(Nat.add(k, n), Nat.add(k, m), d, r) == Nat.divmod.go(n, m, d, Nat.add(k, r)) : Nat & Nat}:
117  match k:
118    case 0n:
119      {==}
120    case 1n+j:
121      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(j, n), Nat.add(j, m), d, 1n+r), Nat.divmod.go(n, m, d, Nat.add(j, 1n+r)), drain(j, n, m, d, 1n+r)) : {_ == Nat.divmod.go(n, m, d, 1n+Nat.add(j, r)) : Nat & Nat}
122      %Broadcast.add_succ(j, r) : {Nat.divmod.go(n, m, d, _) == Nat.divmod.go(n, m, d, 1n+Nat.add(j, r)) : Nat & Nat}
123      {==}