More work on IV Arithmetic, add antimonotonicity of <= and inversion since it was not in HOL4 base library