NatOrder.scale: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
Lines 111-117 of bend-kit-collections@0.1.4.1/nat_order.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&start_line=111&end_line=117

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

def scale(k: Nat, +p: Lin, +q: Lin, +v: Vs, +e: LE(F(p, v), F(q, v)))
  -> LE(F(lsc(k, p), v), F(lsc(k, q), v)):
  match k:
    case 0n:
      MNat.le_refl(F(L{0n, 0n, 0n, 0n, 0n}, v))
    case 1n+ +j:
      comb(p, q, lsc(j, p), lsc(j, q), v, e, scale(j, p, q, v, e))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=F
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Lin
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Vs
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=comb
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=lsc
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_refl