def AP.lt_one

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

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

import Base

96def AP.lt_one(x: Nat, e: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
97  match x:
98    case 0n:
99      {==}
100    case 1n+p:
101      match p:
102        case 0n:
103          Empty.absurd({1n == 0n : Nat}, AP.ft(e))
104        case 1n+q:
105          Empty.absurd({2n+q == 0n : Nat}, AP.ft(e))

Uses (5)

Used by (4)