def un.le_not_lt

bend-osdev-u32@0.1.0.0 · PROOF.bend:260

import Base

260def un.le_not_lt(b: Nat, a: Nat, h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.is_lt(a, b) == False{} : Bool}:
261  match b a:
262    case 0n 0n:
263      {==}
264    case 0n 1n+q:
265      {==}
266    case 1n+p 0n:
267      Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, un.ft(h))
268    case 1n+p 1n+q:
269      un.le_not_lt(p, q, h)