[STATEMENT]
lemma of_rat_ceiling [simp]:
  "\<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>
[PROOF STEP]
using of_rat_floor [of "- r"]
[PROOF STATE]
proof (prove)
using this:
\<lfloor>of_rat (- r)\<rfloor> = \<lfloor>- r\<rfloor>

goal (1 subgoal):
 1. \<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>
[PROOF STEP]
by (simp add: of_rat_minus ceiling_def)