HOL.Alethe_Arith_Rewrites