def remainder

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

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

125def remainder(+r: Nat, +m: Nat, -d: Nat, +a: Nat, bound: Shape.LE(r, m)) -> {Nat.divmod.go(r, m, d, a) == (d, Nat.add(r, a)) : Nat & Nat}:
126  match r m:
127    case 0n m:
128      {==}
129    case 1n+p 0n:
130      match bound:
131    case 1n+p 1n+q:
132      %Equal.sym(Nat & Nat, Nat.divmod.go(p, q, d, 1n+a), (d, Nat.add(p, 1n+a)), remainder(p, q, d, 1n+a, bound)) : {_ == (d, 1n+Nat.add(p, a)) : Nat & Nat}
133      %Broadcast.add_succ(p, a) : {(d, _) == (d, 1n+Nat.add(p, a)) : Nat & Nat}
134      {==}