| changeset 67087 | 733017b19de9 |
| parent 67083 | 6b2c0681ef28 |
| child 67118 | ccab07d1196c |
--- a/src/HOL/Euclidean_Division.thy Thu Nov 23 17:03:26 2017 +0000 +++ b/src/HOL/Euclidean_Division.thy Thu Nov 23 17:03:27 2017 +0000 @@ -139,7 +139,7 @@ class euclidean_ring = idom_modulo + euclidean_semiring begin -lemma dvd_diff_commute: +lemma dvd_diff_commute [ac_simps]: "a dvd c - b \<longleftrightarrow> a dvd b - c" proof - have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"