src/HOL/Archimedean_Field.thy
changeset 30102 799b687e4aac
parent 30096 c5497842ee35
child 35028 108662d50512
equal deleted inserted replaced
30098:896fed07349e 30102:799b687e4aac
   389   using ceiling_diff_of_int [of x 1] by simp
   389   using ceiling_diff_of_int [of x 1] by simp
   390 
   390 
   391 
   391 
   392 subsection {* Negation *}
   392 subsection {* Negation *}
   393 
   393 
   394 lemma floor_minus [simp]: "floor (- x) = - ceiling x"
   394 lemma floor_minus: "floor (- x) = - ceiling x"
   395   unfolding ceiling_def by simp
   395   unfolding ceiling_def by simp
   396 
   396 
   397 lemma ceiling_minus [simp]: "ceiling (- x) = - floor x"
   397 lemma ceiling_minus: "ceiling (- x) = - floor x"
   398   unfolding ceiling_def by simp
   398   unfolding ceiling_def by simp
   399 
   399 
   400 end
   400 end