let s be State of SCMPDS ; :: thesis: for m1, m2 being Element of NAT st IC s = m1 + m2 holds
ICplusConst s,(- m2) = m1
let m1, m2 be Element of NAT ; :: thesis: ( IC s = m1 + m2 implies ICplusConst s,(- m2) = m1 )
assume A1: IC s = m1 + m2 ; :: thesis: ICplusConst s,(- m2) = m1
consider m being Element of NAT such that
A2: m = IC s and
A3: ICplusConst s,(- m2) = abs (m + (- m2)) by SCMPDS_2:def 20;
A4: m = m1 + m2 by A1, A2
.= m1 + m2 ;
m1 >= 0 by NAT_1:2;
hence ICplusConst s,(- m2) = m1 by A3, A4, ABSVALUE:def 1
.= m1
.= m1 ;
:: thesis: verum