def le_from_lt

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:33

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

33# a < 1 + b gives a <= b.
34def le_from_lt(+a: Nat, +b: Nat, h: {Nat.is_lt(a, 1n+b) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
35  match a:
36    case 0n:
37      Arith.le_zero(b)
38    case 1n+p:
39      match b:
40        case 0n:
41          Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, Arith.lt_zero(p, h))
42        case 1n+q:
43          le_from_lt(p, q, h)