let a, b be Element of NAT ; :: thesis: a - b <= a
a - b <= a - 0 by XREAL_1:15;
hence a - b <= a ; :: thesis: verum