ProofShift.ns.le_of_not_lt: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift
Lines 84-93 of bend-osdev-word64@0.1.1.0/proof_shift.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&start_line=84&end_line=93

import Base

def ns.le_of_not_lt(k: Nat, n: Nat, e: {Nat.is_lt(k, n) == False{} : Bool}) -> {Nat.is_le(n, k) == True{} : Bool}:
  match k n:
    case 0n 0n:
      {==}
    case 0n 1n+ +q:
      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, ns.tf(e))
    case 1n+ +p 0n:
      {==}
    case 1n+ +p 1n+ +q:
      ns.le_of_not_lt(p, q, e)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.tf