src/HOL/Real.thy
changeset 66793 deabce3ccf1f
parent 66515 85c505c98332
child 66912 a99a7cbf0fb5
     1.1 --- a/src/HOL/Real.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -23,6 +23,11 @@
     1.4  
     1.5  subsection \<open>Preliminary lemmas\<close>
     1.6  
     1.7 +text{*Useful in convergence arguments*}
     1.8 +lemma inverse_of_nat_le:
     1.9 +  fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
    1.10 +  by (simp add: frac_le)
    1.11 +
    1.12  lemma inj_add_left [simp]: "inj (op + x)"
    1.13    for x :: "'a::cancel_semigroup_add"
    1.14    by (meson add_left_imp_eq injI)