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