def wn.le_not_lt

bend-osdev-word64@0.1.1.0 · proof_value.bend:205

import Base

205def wn.le_not_lt(b: Nat, a: Nat, h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.is_lt(a, b) == False{} : Bool}:
206  match b a:
207    case 0n 0n:
208      {==}
209    case 0n 1n+q:
210      {==}
211    case 1n+p 0n:
212      Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, wn.ft(h))
213    case 1n+p 1n+q:
214      wn.le_not_lt(p, q, h)