~/jendhub

def un.add_lt_absurd

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

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

256# x + k < k never holds
257def un.add_lt_absurd(+s: Nat, +k: Nat, h: {Nat.is_lt(Nat.add(s, k), k) == True{} : Bool}) -> Empty:
258  un.ft(Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(s, k), k), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(s, k), k), False{}, un.not_lt_add_l(s, k)), h))

Uses (9)

Used by (1)