def ns.le_of_not_lt

bend-osdev-word64@0.1.1.0 · proof_shift.bend:84

import Base

84def ns.le_of_not_lt(k: Nat, n: Nat, e: {Nat.is_lt(k, n) == False{} : Bool}) -> {Nat.is_le(n, k) == True{} : Bool}:
85  match k n:
86    case 0n 0n:
87      {==}
88    case 0n 1n+ +q:
89      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, ns.tf(e))
90    case 1n+ +p 0n:
91      {==}
92    case 1n+ +p 1n+ +q:
93      ns.le_of_not_lt(p, q, e)