ConstructProofs.scale_within: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend as ConstructProofs
Lines 20-25 of bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&start_line=20&end_line=25

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

def scale_within(+head: Nat, -tail: List<&2, Nat>, +size: Nat, -exact: {size == Shape.numel(tail) : Nat}, +small: Shape.BoolCase<Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n))>, fits_small: {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n)) : Bool}, fits_product: {True{} == Nat.is_le(Nat.mul(head, size), 1048576n) : Bool}) -> {True{} == within(head <> tail, Shape.capacity.scale(head, tail, size, exact, small)) : Bool}:
  match small:
    case Shape.BFalse{equal}:
      Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n)), fits_small, equal))
    case Shape.BTrue{equal}:
      bound_within(head <> tail, Nat.mul(head, size), Equal.cong(Nat, Nat, value => Nat.mul(head, value), size, Shape.numel(tail), exact), Shape.bool_case(Nat.is_le(Nat.mul(head, size), 1048576n)), fits_product)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  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/shape/construct_proofs.bend&name=bound_within
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&name=within
  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/shape/core.bend&name=bool_case
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=capacity.scale
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=contradiction