src/HOL/Divides.thy
changeset 64244 e7102c40783c
parent 64243 aee949f6642d
child 64246 15d1ee6e847b
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -1117,7 +1117,7 @@
     1.4  lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
     1.5  by (simp add: le_mod_geq)
     1.6  
     1.7 -lemma mod_1 [simp]: "m mod Suc 0 = 0"
     1.8 +lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
     1.9  by (induct m) (simp_all add: mod_geq)
    1.10  
    1.11  (* a simple rearrangement of div_mult_mod_eq: *)
    1.12 @@ -1196,7 +1196,7 @@
    1.13  
    1.14  subsubsection \<open>Further Facts about Quotient and Remainder\<close>
    1.15  
    1.16 -lemma div_1 [simp]:
    1.17 +lemma div_by_Suc_0 [simp]:
    1.18    "m div Suc 0 = m"
    1.19    using div_by_1 [of m] by simp
    1.20