src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 64240 eabf80376aab
parent 64177 006f303fb173
child 64242 93c6f0da5c70
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
     1.5  begin
     1.6  
     1.7 -lemma zero_mod_left [simp]: "0 mod a = 0"
     1.8 +lemma mod_0 [simp]: "0 mod a = 0"
     1.9    using mod_div_equality [of 0 a] by simp
    1.10  
    1.11  lemma dvd_mod_iff: