let k, n be Nat; :: thesis: n - k <= n
n <= n + k by NAT_1:11;
hence n - k <= n by XREAL_1:20; :: thesis: verum