def cover

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

import Base
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

206def cover(+rest: Nat, +step: Nat, positive: {Nat.is_lt(0n, step) == True{} : Bool}) ->
207  {Nat.is_le(1n+rest, Nat.add(step, Nat.mul(Nat.div(rest, step), step))) == True{} : Bool}:
208  match step:
209    case 0n:
210      Empty.absurd({Nat.is_le(1n+rest, Nat.add(0n, Nat.mul(Nat.div(rest, 0n), 0n))) == True{} : Bool}, Arith.clash(positive))
211    case 1n+s:
212      covered(rest, s, Fiber.decompose(rest, 1n+s, {==}))