equal
deleted
inserted
replaced
853 simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) |
853 simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) |
854 |
854 |
855 |
855 |
856 subsubsection {* More results about difference *} |
856 subsubsection {* More results about difference *} |
857 |
857 |
858 lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0" |
|
859 by (induct m) simp_all |
|
860 |
|
861 text {* Addition is the inverse of subtraction: |
858 text {* Addition is the inverse of subtraction: |
862 if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *} |
859 if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *} |
863 lemma add_diff_inverse: "~ m < n ==> n + (m - n) = (m::nat)" |
860 lemma add_diff_inverse: "~ m < n ==> n + (m - n) = (m::nat)" |
864 by (induct m n rule: diff_induct) simp_all |
861 by (induct m n rule: diff_induct) simp_all |
865 |
862 |