let s be State of SCMPDS; :: thesis: for m, n being Nat st IC s = m holds

ICplusConst (s,(n - m)) = n

let m, n be 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)) = |.(k + (n - m)).| ) by SCMPDS_2:def 18;

hence ( IC s = m implies ICplusConst (s,(n - m)) = n ) by ABSVALUE:def 1; :: thesis: verum

ICplusConst (s,(n - m)) = n

let m, n be 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)) = |.(k + (n - m)).| ) by SCMPDS_2:def 18;

hence ( IC s = m implies ICplusConst (s,(n - m)) = n ) by ABSVALUE:def 1; :: thesis: verum