def not_lt_le

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:163

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

163# is_lt(a, b) == False gives b <= a.
164def not_lt_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.is_le(b, a) == True{} : Bool}:
165  match a b:
166    case _ 0n:
167      zero_le(a)
168    case 0n 1n+q:
169      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, L.true_false(e))
170    case 1n+p 1n+q:
171      not_lt_le(p, q, e)