def scale

bend-kit-collections@0.1.4.1 · nat_order.bend:111

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

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