def AP.not_lt_le

bend-osdev-array@0.1.0.1 · PROOF.bend:85

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

85def AP.not_lt_le(x: Nat, y: Nat, e: {Nat.is_lt(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
86  match x y:
87    case 0n 0n:
88      {==}
89    case 0n 1n+q:
90      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, AP.tf(e))
91    case 1n+p 0n:
92      {==}
93    case 1n+p 1n+q:
94      AP.not_lt_le(p, q, e)

Uses (6)

Used by (1)

bend-osdev-array@0.1.0.1/PROOF:AP.split