src/HOL/Computational_Algebra/Euclidean_Algorithm.thy

     by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
   show "(Euclidean_Algorithm.Gcd :: nat set \<Rightarrow> _) = Gcd"
     by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
 qed
 
+lemma prime_factorization_Suc_0 [simp]: "prime_factorization (Suc 0) = {#}"
+  unfolding One_nat_def [symmetric] using prime_factorization_1 .
+
 instance int :: normalization_euclidean_semiring ..
 
 instance int :: euclidean_ring_gcd
 proof
   interpret semiring_Gcd 1 0 times