src/HOL/GCD.thy

--- a/src/HOL/GCD.thy	Mon Jan 29 21:18:11 2024 +0100
+++ b/src/HOL/GCD.thy	Tue Jan 30 16:39:21 2024 +0000
@@ -2942,4 +2942,11 @@
   in [(\<^const_syntax>\<open>semiring_char\<close>, char_type_tr')] end
 \<close>
 
+
+lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \<noteq> Suc 0"
+  by (metis One_nat_def of_nat_1 of_nat_CHAR zero_neq_one)
+
+lemma (in idom) CHAR_not_1' [simp]: "CHAR('a) \<noteq> Suc 0"
+  using local.of_nat_CHAR by fastforce
+
 end