def cvle

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

import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder

import Base

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

Uses (5)

Used by (36)