def un.nlt_le

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

import Base

1514# not x < y: y <= x
1515def un.nlt_le(x: Nat, y: Nat, e: {Nat.is_lt(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
1516  match x y:
1517    case 0n 0n:
1518      {==}
1519    case 0n 1n+q:
1520      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, un.tf(e))
1521    case 1n+p 0n:
1522      {==}
1523    case 1n+p 1n+q:
1524      un.nlt_le(p, q, e)