# Re: [PVS-Help] Regarding floor and ceiling of reals

```Nikhil D. Kikkeri writes:

Lets assume I have a real number x > 1 and x < 2

Now I would assume that 2^-52*ceiling(x*2^52) would be less than or equal to
2

Now if this is true (and i think it is), why am I finding it difficult to
prove this as a lemma? Grind just expands "^"

You have to invest a bit more. I prove

c : Lemma Forall(x : real) :
x > 1 And x < 2 Implies
2^-52 * ceiling(x*2^52) <= 2

with

;;; Proof c-1 for formula A.c
;;; developed with shostak decision procedures
(""
(skosimp* :preds? t)
(use "ceiling_def")
(flatten)
(case "ceiling(x!1 * 2 ^ 52) <= 2 * 2 ^ 52")
(("1"
(hide-all-but (-1 1))
(use "both_sides_times_pos_le1" :subst
("x" "ceiling(x!1 * 2 ^ 52)" "y" "2 * 2 ^ 52" "pz" "2^-52"))
(assert)
(rewrite "expt_plus" :dir rl)
(rewrite "expt_x0")
(assert))
("2"
(hide 2)
(use "both_sides_times_pos_lt1" :subst ("x" "x!1" "y" "2"))
(use "both_sides_plus_lt2" :subst
("x" "x!1 * 2 ^ 52" "y" "2 * 2 ^ 52" "z" "1"))
(name-replace "xx" "2*2^52")
(assert))))

Bye,

Hendrik

```