def lt_positive

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

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

45# a < b gives 1 <= b.
46def lt_positive(+a: Nat, +b: Nat, h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(1n, b) == True{} : Bool}:
47  match b:
48    case 0n:
49      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, Arith.lt_zero(a, h))
50    case 1n+q:
51      Arith.le_zero(q)