theorem Th2: :: SCMP_GCD:2

for s being State of SCMPDS
for m1, m2 being Nat st IC s = m1 + m2 holds
ICplusConst (s,(- m2)) = m1