src/HOL/Real.thy
changeset 61204 3e491e34a62e
parent 61076 bdc1e2f0a86a
child 61284 2314c2f62eb1
     1.1 --- a/src/HOL/Real.thy	Mon Sep 21 14:44:32 2015 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Sep 21 19:52:13 2015 +0100
     1.3 @@ -22,6 +22,13 @@
     1.4  
     1.5  subsection \<open>Preliminary lemmas\<close>
     1.6  
     1.7 +lemma inj_add_left [simp]: 
     1.8 +  fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)"
     1.9 +by (meson add_left_imp_eq injI)
    1.10 +
    1.11 +lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
    1.12 +  by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
    1.13 +
    1.14  lemma add_diff_add:
    1.15    fixes a b c d :: "'a::ab_group_add"
    1.16    shows "(a + c) - (b + d) = (a - b) + (c - d)"