# HG changeset patch
# User haftmann
# Date 1580070931 0
# Node ID 2525e28e4b8b56dc355728ea27358c9a1538f80f
# Parent  3887432720a977dc5c4db03a792819c04e8dd643
generalized

diff -r 3887432720a9 -r 2525e28e4b8b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Jan 26 20:35:30 2020 +0000
+++ b/src/HOL/Nat.thy	Sun Jan 26 20:35:31 2020 +0000
@@ -1696,11 +1696,17 @@
 
 declare of_nat_code [code]
 
-context ring_1
+context semiring_1_cancel
 begin
 
-lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
-  by (simp add: algebra_simps of_nat_add [symmetric])
+lemma of_nat_diff:
+  \<open>of_nat (m - n) = of_nat m - of_nat n\<close> if \<open>n \<le> m\<close>
+proof -
+  from that obtain q where \<open>m = n + q\<close>
+    by (blast dest: le_Suc_ex)
+  then show ?thesis
+    by simp
+qed
 
 end