let a, b be Nat; :: thesis: a - b <= a
a - b <= a - 0 by XREAL_1:13;
hence a - b <= a ; :: thesis: verum