# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1660564224 -3600
# Node ID 62c64e3e47410964cb6f82ea08f75513b5f0c43c
# Parent  3842556b757c755af4fa339ad8cbb7da7e217fe9
The same, without adding a new simprule

diff -r 3842556b757c -r 62c64e3e4741 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sun Aug 14 23:51:47 2022 +0100
+++ b/src/HOL/Binomial.thy	Mon Aug 15 12:50:24 2022 +0100
@@ -1066,7 +1066,8 @@
   assumes "k \<le> n"
   shows "(of_nat :: (nat \<Rightarrow> ('a :: field_char_0))) (n choose k) = of_nat (n + 1 - k) / of_nat (n + 1) * of_nat (Suc n choose k)"
 proof (cases k)
-  case 0 then show ?thesis by simp
+  case 0 then show ?thesis
+    using of_nat_neq_0 by auto
 next
   case (Suc l)
   have "of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
@@ -1077,7 +1078,7 @@
   also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
     by (simp only: Suc_eq_plus1)
   finally have "(\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
-    by (simp add: field_simps)
+    using of_nat_neq_0 by (auto simp: mult.commute divide_simps)
   with assms show ?thesis
     by (simp add: binomial_altdef_of_nat prod_dividef)
 qed
diff -r 3842556b757c -r 62c64e3e4741 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Sun Aug 14 23:51:47 2022 +0100
+++ b/src/HOL/Factorial.thy	Mon Aug 15 12:50:24 2022 +0100
@@ -64,11 +64,7 @@
   by (cases n) auto
 
 lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
-  apply (induct n)
-  apply auto
-  using of_nat_eq_0_iff
-  apply fastforce
-  done
+  using of_nat_0_neq by (induct n) auto
 
 lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
   by (induct n) (auto simp: le_Suc_eq)
diff -r 3842556b757c -r 62c64e3e4741 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Aug 14 23:51:47 2022 +0100
+++ b/src/HOL/Nat.thy	Mon Aug 15 12:50:24 2022 +0100
@@ -1768,14 +1768,6 @@
 lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
   by (auto intro: inj_of_nat injD)
 
-lemma one_plus_of_nat_neq_zero [simp]:
-  "1 + of_nat n \<noteq> 0"
-proof -
-  have "of_nat (Suc n) \<noteq> of_nat 0"
-    unfolding of_nat_eq_iff by simp
-  then show ?thesis by simp
-qed
-
 text \<open>Special cases where either operand is zero\<close>
 
 lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"