# HG changeset patch
# User haftmann
# Date 1664874758 0
# Node ID c9ea813f92f217b965b2c303bfee793542385a99
# Parent  4111c94657b4fc5404bf01c18be57750ea789c9f
tuned proof

diff -r 4111c94657b4 -r c9ea813f92f2 src/HOL/Euclidean_Division.thy
--- 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>
-    by (simp add: div_eq_0_iff)
-  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
-      by (subst div_add1_eq) auto
-  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>
         by (subst mod_add_left_eq [symmetric]) simp
@@ -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
+      by (simp add: div_eq_0_iff)
+  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
-      by (subst div_add1_eq) (auto simp add: div_eq_0_iff mod_greater_zero_iff_not_dvd)
   qed
-  then show ?thesis
-    by simp
+  finally show ?thesis
+    by (simp add: mod_greater_zero_iff_not_dvd)
 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>
     by (simp add: mod_simps)
-  also have "\<dots> = ?rhs"
-    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
-  finally show ?thesis .
+  ultimately show ?thesis
+    by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
 qed
 
 lemma Suc_times_mod_eq: