HOL.Alethe_Arith_Real_Rewrites