def le_true

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

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

9def le_true(+a: Nat, +b: Nat, bound: Shape.LE(a, b)) -> {True{} == Nat.is_le(a, b) : Bool}:
10  match a b:
11    case 0n 0n:
12      {==}
13    case 0n 1n+q:
14      {==}
15    case 1n+p 0n:
16      match bound:
17    case 1n+p 1n+q:
18      le_true(p, q, bound)