~/jendhub

def un.lt1

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

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base

2052def un.lt1(x: Nat, h: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
2053  match x:
2054    case 0n:
2055      {==}
2056    case 1n+ +p:
2057      match p:
2058        case 0n:
2059          Empty.absurd({1n == 0n : Nat}, un.ft(h))
2060        case 1n+ +q:
2061          Empty.absurd({2n+q == 0n : Nat}, un.ft(h))

Uses (5)

Used by (1)