let n, k be Element of NAT ; :: thesis: n - k <= n
n <= n + k by NAT_1:11;
hence n - k <= n by XREAL_1:22; :: thesis: verum