def div_below

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:177

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

177def div_below(+t: Nat, +a: Nat, +size: Nat, +below: {Nat.is_lt(t, Nat.mul(a, size)) == True{} : Bool}) ->
178  {Nat.is_lt(Nat.div(t, size), a) == True{} : Bool}:
179  quotient_below(t, a, size, below, Shape.bool_case(Nat.is_lt(Nat.div(t, size), a)), decompose(t, size, positive_of(t, a, size, below)))