let s be State of SCMPDS; :: thesis: for m, n being Element of NAT st IC s = m holds
ICplusConst (s,(n - m)) = n
let m, n be Element of NAT ; :: thesis: ( IC s = m implies ICplusConst (s,(n - m)) = n )
ex k being Element of NAT st
( k = IC s & ICplusConst (s,(n - m)) = abs (k + (n - m)) ) by SCMPDS_2:def 18;
hence ( IC s = m implies ICplusConst (s,(n - m)) = n ) by ABSVALUE:def 1; :: thesis: verum