author haftmann Tue, 04 Oct 2022 09:12:38 +0000 changeset 76246 c9ea813f92f2 parent 76245 4111c94657b4 child 76247 e19d4c1c48ce
tuned proof
```--- a/src/HOL/Euclidean_Division.thy	Tue Oct 04 09:12:34 2022 +0000
+++ b/src/HOL/Euclidean_Division.thy	Tue Oct 04 09:12:38 2022 +0000
@@ -1411,7 +1411,7 @@
using div_less_iff_less_mult [of q n m] that by auto

lemma div_Suc:
-  \<open>Suc m div n = (if Suc m mod n = 0 then Suc (m div n) else m div n)\<close>  (is "_ = ?rhs")
+  \<open>Suc m div n = (if Suc m mod n = 0 then Suc (m div n) else m div n)\<close>
proof (cases \<open>n = 0 \<or> n = 1\<close>)
case True
then show ?thesis by auto
@@ -1419,34 +1419,15 @@
case False
then have \<open>n > 1\<close>
by simp
-  then have *: \<open>Suc 0 div n = 0\<close>
-  have \<open>(m + 1) div n = ?rhs\<close>
+  then have \<open>Suc m div n = m div n + Suc (m mod n) div n\<close>
+    using div_add1_eq [of m 1 n] by simp
+  also have \<open>Suc (m mod n) div n = of_bool (n dvd Suc m)\<close>
proof (cases \<open>n dvd Suc m\<close>)
-    case True
-    then obtain q where \<open>Suc m = n * q\<close> ..
-    then have m: \<open>m = n * q - 1\<close>
-      by simp
-    have \<open>q > 0\<close> by (rule ccontr)
-      (use \<open>Suc m = n * q\<close> in simp)
-    from m have \<open>m mod n = (n * q - 1) mod n\<close>
-      by simp
-    also have \<open>\<dots> = (n * q - 1 + n) mod n\<close>
-      by simp
-    also have \<open>n * q - 1 + n = n * q + (n - 1)\<close>
-      using \<open>n > 1\<close> \<open>q > 0\<close> by (simp add: algebra_simps)
-    finally have \<open>m mod n = (n - 1) mod n\<close>
-      by simp
-    with \<open>n > 1\<close> have \<open>m mod n = n - 1\<close>
-      by simp
-    with True \<open>n > 1\<close> show ?thesis
-  next
case False
-    have \<open>Suc (m mod n) \<noteq> n\<close>
+    moreover have \<open>Suc (m mod n) \<noteq> n\<close>
proof (rule ccontr)
assume \<open>\<not> Suc (m mod n) \<noteq> n\<close>
-      then have \<open>m mod n = n - 1\<close>
+      then have \<open>m mod n = n - Suc 0\<close>
by simp
with \<open>n > 1\<close> have \<open>(m + 1) mod n = 0\<close>
@@ -1456,28 +1437,35 @@
qed
moreover have \<open>Suc (m mod n) \<le> n\<close>
using \<open>n > 1\<close> by (simp add: Suc_le_eq)
-    ultimately have \<open>Suc (m mod n) < n\<close>
+    ultimately show ?thesis
+  next
+    case True
+    then obtain q where q: \<open>Suc m = n * q\<close> ..
+    moreover have \<open>q > 0\<close> by (rule ccontr)
+      (use q in simp)
+    ultimately have \<open>m mod n = n - Suc 0\<close>
+      using \<open>n > 1\<close> mult_le_cancel1 [of n \<open>Suc 0\<close> q]
+      by (auto intro: mod_nat_eqI)
+    with True \<open>n > 1\<close> show ?thesis
by simp
-    with False \<open>n > 1\<close> show ?thesis
qed
-  then show ?thesis
-    by simp
+  finally show ?thesis
qed

lemma mod_Suc:
-  \<open>Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))\<close>  (is "_ = ?rhs")
-proof (cases "n = 0")
+  \<open>Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))\<close>
+proof (cases \<open>n = 0\<close>)
case True
then show ?thesis
by simp
next
case False
-  have "Suc m mod n = Suc (m mod n) mod n"
+  moreover have \<open>Suc m mod n = Suc (m mod n) mod n\<close>