~/jendhub

def nat.sub_le

bend-osdev-algo@0.1.0.0 · PROOF.bend:137

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
import Base

137def nat.sub_le(n: Nat, k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
138  match n k:
139    case 0n _:
140      {==}
141    case 1n+np 0n:
142      nat.le_refl(np)
143    case 1n+ +np 1n+ +kp:
144      nat.le_succ(Nat.sub(np, kp), np, nat.sub_le(np, kp))

Uses (6)

Used by (1)