PROOF.un.add_lt_absurd: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 256-258 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=256&end_line=258

import Base

# x + k < k never holds
def un.add_lt_absurd(+s: Nat, +k: Nat, h: {Nat.is_lt(Nat.add(s, k), k) == True{} : Bool}) -> Empty:
  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):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.not_lt_add_l