HOL-ex.Arith_Examples