NatOrder.cvle: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
Lines 205-209 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=205&end_line=209

import Base

def cvle(-A: Nat, -B: Nat, -p: Lin, -q: Lin, -v: Vs, eA: {A == F(p, v) : Nat}, eB: {B == F(q, v) : Nat},
  h: LE(A, B)) -> LE(F(p, v), F(q, v)):
  %eA : LE(_, F(q, v))
  %eB : LE(A, _)
  h

Uses (5):
  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