def scaled_le

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

import Base
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber

170def scaled_le(+k: Nat, +rest: Nat, +step: Nat, below: {Nat.is_lt(k, 1n+Nat.div(rest, step)) == True{} : Bool}) ->
171  {Nat.is_le(Nat.mul(k, step), rest) == True{} : Bool}:
172  match step:
173    case 0n:
174      %Equal.sym(Nat, Nat.mul(k, 0n), 0n, Nats.mul_zero_right(k)) : {Nat.is_le(_, rest) == True{} : Bool}
175      Arith.le_zero(rest)
176    case 1n+s:
177      scaled_within(k, rest, s, lt_succ_le(k, Nat.div(rest, 1n+s), below), Fiber.decompose(rest, 1n+s, {==}))