def ckp.lt_sub

bend-osdev-acpi@0.1.2.0 · PROOF_checksum.bend:198

import Base
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

198def ckp.lt_sub(+i: Nat, +n: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {Nat.is_le(1n, Nat.sub(n, i)) == True{} : Bool}:
199  match i:
200    case 0n:
201      match n:
202        case 0n:
203          Empty.absurd({Nat.is_le(1n, Nat.sub(0n, 0n)) == True{} : Bool}, ckp.ft(h))
204        case 1n+p:
205          UO.nat_le_add_r(1n, p)
206    case 1n+ip:
207      match n:
208        case 0n:
209          Empty.absurd({Nat.is_le(1n, Nat.sub(0n, 1n+ip)) == True{} : Bool}, ckp.ft(h))
210        case 1n+p:
211          ckp.lt_sub(ip, p, h)