def scaled_within

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:161

import Base
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber

161# k <= rest / step gives k * step <= rest; at step 0 the product is 0.
162def scaled_within(+k: Nat, +rest: Nat, +s: Nat, +k_le: {Nat.is_le(k, Nat.div(rest, 1n+s)) == True{} : Bool},
163  given: Fiber.Decomposed<rest, 1n+s>) -> {Nat.is_le(Nat.mul(k, 1n+s), rest) == True{} : Bool}:
164  Fiber.Decomposed{below, sum} = given
165  Fiber.le_trans(Nat.mul(k, 1n+s), Nat.mul(Nat.div(rest, 1n+s), 1n+s), rest,
166    Fiber.mul_le_mono(k, Nat.div(rest, 1n+s), 1n+s, k_le),
167    %sum : {Nat.is_le(Nat.mul(Nat.div(rest, 1n+s), 1n+s), _) == True{} : Bool}
168    Api.le_add_right(Nat.mul(Nat.div(rest, 1n+s), 1n+s), Nat.mod(rest, 1n+s)))