def nat.nlt_le

bend-osdev-algo@0.1.0.0 · PROOF.bend:958

import Base

958# not a < c, a <= b: not b < c
959def nat.nlt_le(a: Nat, b: Nat, c: Nat, e: {Nat.is_lt(a, c) == False{} : Bool}, f: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(b, c) == False{} : Bool}:
960  match a b c:
961    case 0n _ 0n:
962      nat.lt_zero(b)
963    case 0n _ 1n+cp:
964      Empty.absurd({Nat.is_lt(b, 1n+cp) == False{} : Bool}, absurd.tf(e))
965    case 1n+ap 0n _:
966      Empty.absurd({Nat.is_lt(0n, c) == False{} : Bool}, absurd.ft(f))
967    case 1n+ap 1n+bp 0n:
968      {==}
969    case 1n+ap 1n+bp 1n+cp:
970      nat.nlt_le(ap, bp, cp, e, f)