--- a/src/HOL/Parity.thy Fri Sep 15 20:46:50 2023 +0100
+++ b/src/HOL/Parity.thy Sat Sep 16 06:38:44 2023 +0000
@@ -307,6 +307,12 @@
qed
qed
+lemma mod_double_nat:
+ \<open>n mod (2 * m) = n mod m \<or> n mod (2 * m) = n mod m + m\<close>
+ for m n :: nat
+ by (cases \<open>even (n div m)\<close>)
+ (simp_all add: mod_mult2_eq ac_simps even_iff_mod_2_eq_zero)
+
context semiring_parity
begin
@@ -789,6 +795,10 @@
\<open>of_bool b div 2 = 0\<close>
by simp
+lemma of_nat_mod_double:
+ \<open>of_nat n mod (2 * of_nat m) = of_nat n mod of_nat m \<or> of_nat n mod (2 * of_nat m) = of_nat n mod of_nat m + of_nat m\<close>
+ by (simp add: mod_double_nat flip: of_nat_mod of_nat_add of_nat_mult of_nat_numeral)
+
end
class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat