ReduceFiberProof.mask_at: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 194-204 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=194&end_line=204

import Base
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

# On a kept row of left stride `size`, the position with digit d and
# walk w below size lands on t exactly when d is t's quotient and w its
# remainder.
def mask_at(+size: Nat, +d: Nat, +w: Nat, +t: Nat, given: Decomposed<t, size>, same: {d == Nat.div(t, size) : Nat}) ->
  {Nat.is_eq(Nat.add(Nat.mul(size, d), w), t) == Nat.is_eq(w, Nat.mod(t, size)) : Bool}:
  Decomposed{below, sum} = given
  %sum :
    {Nat.is_eq(Nat.add(Nat.mul(size, d), w), _) == Nat.is_eq(w, Nat.mod(t, size)) : Bool}
  %same : {Nat.is_eq(Nat.add(Nat.mul(size, d), w), Nat.add(Nat.mul(_, size), Nat.mod(t, size))) == Nat.is_eq(w, Nat.mod(t, size)) : Bool}
  %Nats.mul_comm(size, d) : {Nat.is_eq(Nat.add(Nat.mul(size, d), w), Nat.add(_, Nat.mod(t, size))) == Nat.is_eq(w, Nat.mod(t, size)) : Bool}
  eq_add_cancel(Nat.mul(size, d), w, Nat.mod(t, size))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=Decomposed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=eq_add_cancel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=mul_comm