~/jendhub

def ns.sub_le

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

import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift
import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

74# n - k <= n
75def ns.sub_le(n: Nat, k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
76  match n k:
77    case 0n _:
78      {==}
79    case 1n+ +p 0n:
80      UL.nat_le_refl(1n+p)
81    case 1n+ +p 1n+ +q:
82      UO.nat_le_trans(Nat.sub(p, q), p, 1n+p, ns.sub_le(p, q), ns.le_succ_self(p))

Uses (7)

Used by (1)