let i, j be Nat; :: thesis: ( j < i implies (i -' (j + 1)) + 1 = i -' j )
assume A1: j < i ; :: thesis: (i -' (j + 1)) + 1 = i -' j
then j + 1 <= i by NAT_1:13;
hence (i -' (j + 1)) + 1 = (i - (j + 1)) + 1 by XREAL_1:233
.= i - j
.= i -' j by A1, XREAL_1:233 ;
:: thesis: verum