src/HOL/Num.thy
changeset 58512 dc4d76dfa8f0
parent 58421 37cbbd8eb460
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Num.thy	Thu Oct 02 11:33:05 2014 +0200
     1.2 +++ b/src/HOL/Num.thy	Thu Oct 02 11:33:06 2014 +0200
     1.3 @@ -1073,6 +1073,22 @@
     1.4  lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
     1.5  
     1.6  
     1.7 +subsection {* Particular lemmas concerning @{term 2} *}
     1.8 +
     1.9 +context linordered_field_inverse_zero
    1.10 +begin
    1.11 +
    1.12 +lemma half_gt_zero_iff:
    1.13 +  "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
    1.14 +  by (auto simp add: field_simps)
    1.15 +
    1.16 +lemma half_gt_zero [simp]:
    1.17 +  "0 < a \<Longrightarrow> 0 < a / 2"
    1.18 +  by (simp add: half_gt_zero_iff)
    1.19 +
    1.20 +end
    1.21 +
    1.22 +
    1.23  subsection {* Numeral equations as default simplification rules *}
    1.24  
    1.25  declare (in numeral) numeral_One [simp]