ReduceFiberProof.split_step: 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 47-62 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=47&end_line=62

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
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

def split_step(+t: Nat, +size: Nat, +q: Nat, +r: Nat, below: {Nat.is_lt(r, size) == True{} : Bool},
  sum: {Nat.add(Nat.mul(q, size), r) == t : Nat}, last: Shape.BoolCase<Nat.is_lt(1n+r, size)>) -> Split<1n+t, size>:
  match last:
    case Shape.BTrue{equal}:
      Split{q, 1n+r, Equal.sym(Bool, True{}, Nat.is_lt(1n+r, size), equal),
        Equal.trans(Nat, Nat.add(Nat.mul(q, size), 1n+r), 1n+Nat.add(Nat.mul(q, size), r), 1n+t,
          Arith.add_succ(Nat.mul(q, size), r), Equal.cong(Nat, Nat, n => 1n+n, Nat.add(Nat.mul(q, size), r), t, sum))}
    case Shape.BFalse{equal}:
      +whole = lt_succ_eq(r, size, below, equal)
      Split{1n+q, 0n,
        %Equal.sym(Nat, size, 1n+r, whole) : {Nat.is_lt(0n, _) == True{} : Bool}
        {==},
        %Equal.sym(Nat, Nat.add(Nat.mul(1n+q, size), 0n), Nat.mul(1n+q, size), Broadcast.add_zero(Nat.mul(1n+q, size))) : {_ == 1n+t : Nat}
        %Equal.sym(Nat, size, 1n+r, whole) : {Nat.add(_, Nat.mul(q, size)) == 1n+t : Nat}
        %Equal.sym(Nat, Nat.add(r, Nat.mul(q, size)), Nat.add(Nat.mul(q, size), r), add_comm(r, Nat.mul(q, size))) : {1n+_ == 1n+t : Nat}
        Equal.cong(Nat, Nat, n => 1n+n, Nat.add(Nat.mul(q, size), r), t, sum)}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.is_lt
  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=Split
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=lt_succ_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ