src/HOL/Archimedean_Field.thy
changeset 63597 bef0277ec73b
parent 63540 f8652d0534fa
child 63599 f560147710fb
     1.1 --- a/src/HOL/Archimedean_Field.thy	Fri Aug 05 09:05:03 2016 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Fri Aug 05 09:30:20 2016 +0200
     1.3 @@ -642,6 +642,9 @@
     1.4      by (auto simp add: frac_def algebra_simps)
     1.5  qed
     1.6  
     1.7 +lemma floor_add2[simp]: "frac x = 0 \<or> frac y = 0 \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
     1.8 +by (metis add.commute add.left_neutral frac_lt_1 floor_add)
     1.9 +
    1.10  lemma frac_add:
    1.11    "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y else (frac x + frac y) - 1)"
    1.12    by (simp add: frac_def floor_add)