def lt_le

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:107

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

107def lt_le(+a: Nat, +b: Nat, bound: Shape.LT(a, 1n+b)) -> Shape.LE(a, b):
108  match a b:
109    case 0n b:
110      Unit{}
111    case 1n+p 0n:
112      Empty.absurd(Empty, lt_zero(p, bound))
113    case 1n+p 1n+q:
114      lt_le(p, q, bound)