let i, k be Nat; :: thesis: ( 1 <= i & 1 <= k implies (k -' i) + 1 <= k )
assume that
A1: 1 <= i and
A2: 1 <= k ; :: thesis: (k -' i) + 1 <= k
k -' i <= k -' 1 by A1, NAT_D:41;
then (k -' i) + 1 <= (k -' 1) + 1 by XREAL_1:6;
hence (k -' i) + 1 <= k by A2, XREAL_1:235; :: thesis: verum