Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-29 16:52:27 -0800 (Sat, 29 Mar 2003)
1.Now arithT can deal with equality in conclusion (now it support lt,gt,le,ge,eq). neq is still unsupported.
2.As much as possible of substitution reasoning is replaced with arithT in itt_nat/int_div_rem.
P.S. I know that number of steps is alarmingly high, I'll look into it now.