def not_le_lt

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

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

191def not_le_lt(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == False{} : Bool}) -> {Nat.is_lt(b, a) == True{} : Bool}:
192  match a b:
193    case 0n 0n:
194      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(e))
195    case 0n 1n+q:
196      Empty.absurd({Nat.is_lt(1n+q, 0n) == True{} : Bool}, L.true_false(e))
197    case 1n+p 0n:
198      {==}
199    case 1n+p 1n+q:
200      not_le_lt(p, q, e)