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)