let k, i, j be natural Number ; :: thesis: ( i <= j implies (j + k) -' i = (j -' i) + k )
assume A1: i <= j ; :: thesis: (j + k) -' i = (j -' i) + k
hence (j + k) -' i = (j + k) - i by NAT_1:12, XREAL_1:233
.= (j - i) + k
.= (j -' i) + k by A1, XREAL_1:233 ;
:: thesis: verum