Remove/Name Anonymous Rewrite for NUM_CEILING

[jdyeager]

For the constant clg defined in realTheory.NUM_CEILING_def, there is currently an anonymous automatic rewrite presumably derived from realTheory.NUM_CEILING_NUM_FLOOR.
From a simplifier trace:
[rewrite:<anonymous>]⊢ clg r = (let n = flr r in if r ≤ 0 ∨ r = &n then n else n + 1)

This is an awkward and somewhat unpleasant form to work with. It automatically expanding also dramatically bloats the goal statement. In my particular case, clg (logr 4 (real_of_rat ((est * est − x) / (tol * tol)))) becomes:

if
  logr 4 (real_of_rat ((est * est − x) / (tol * tol))) ≤ 0 ∨
  logr 4 (real_of_rat ((est * est − x) / (tol * tol))) =
  &flr (logr 4 (real_of_rat ((est * est − x) / (tol * tol))))
then
  flr (logr 4 (real_of_rat ((est * est − x) / (tol * tol))))
else flr (logr 4 (real_of_rat ((est * est − x) / (tol * tol)))) + 1

Which is mildly obscene to look at or reason about, especially when compared with the actual definition:
⊢ ∀x. clg x = LEAST n. x ≤ &n

I think it would be good to remove this automatic rewrite. But at the very least I feel it should be named to make it excludable.

[mn200]

I will definitely remove it as automatic. It's clearly only meant to expand for concrete arguments so that the simplifier can evaluate those.