def off.le_sub

bend-osdev-bytes@0.1.1.0 · PROOF.bend:795

import Base

795# i + n <= m: n <= m - i
796def off.le_sub(+i: Nat, +n: Nat, +m: Nat) -> {Nat.is_le(Nat.add(i, n), m) == True{} : Bool} -> {Nat.is_le(n, Nat.sub(m, i)) == True{} : Bool}:
797  match i m:
798    case 0n 0n:
799      h => h
800    case 0n 1n+q:
801      h => h
802    case 1n+p 0n:
803      h => off.no({Nat.is_le(n, Nat.sub(0n, 1n+p)) == True{} : Bool}, h)
804    case 1n+p 1n+q:
805      h => off.le_sub(p, n, q, h)