ReduceFiberProof.decomposed: 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 96-105 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=96&end_line=105

import Base

def decomposed(+t: Nat, +size: Nat, given: Split<t, size>) -> Decomposed<t, size>:
  Split{+q, +r, +below, +sum} = given
  +dq = div_of(t, size, q, r, below, sum)
  +dr = mod_of(t, size, q, r, below, sum)
  Decomposed{
    %Equal.sym(Nat, Nat.mod(t, size), r, dr) : {Nat.is_lt(_, size) == True{} : Bool}
    below,
    %Equal.sym(Nat, Nat.div(t, size), q, dq) : {Nat.add(Nat.mul(_, size), Nat.mod(t, size)) == t : Nat}
    %Equal.sym(Nat, Nat.mod(t, size), r, dr) : {Nat.add(Nat.mul(q, size), _) == t : Nat}
    sum}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_lt
  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=Split
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=div_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=mod_of