~/jendhub

def off.le_add_l

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

import bend-osdev-bytes@0.1.1.0/PROOF.bend as PROOF
import Base

785# i + n <= m: i <= m
786def off.le_add_l(+i: Nat, +n: Nat, +m: Nat) -> {Nat.is_le(Nat.add(i, n), m) == True{} : Bool} -> {Nat.is_le(i, m) == True{} : Bool}:
787  match i m:
788    case 0n _:
789      h => off.le_zero(m)
790    case 1n+p 0n:
791      h => off.no({Nat.is_le(1n+p, 0n) == True{} : Bool}, h)
792    case 1n+p 1n+q:
793      h => off.le_add_l(p, n, q, h)

Uses (6)

Used by (1)