~/jendhub

def AP.lt_le

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

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

767def AP.lt_le(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
768  match x y:
769    case 0n 0n:
770      {==}
771    case 0n 1n+q:
772      {==}
773    case 1n+p 0n:
774      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, AP.ft(h))
775    case 1n+p 1n+q:
776      AP.lt_le(p, q, h)

Uses (6)

Used by (1)