src/HOL/Divides.thy
 changeset 66801 f3fda9777f9a parent 66800 128e9ed9f63c child 66806 a4e82b58d833
```     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:19 2017 +0200
1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:20 2017 +0200
1.3 @@ -1627,12 +1627,8 @@
1.4    from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
1.5  qed
1.6
1.7 -lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
1.8 -proof -
1.9 -  have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
1.10 -  also have "... = Suc m mod n" by (rule mod_mult_self3)
1.11 -  finally show ?thesis .
1.12 -qed
1.13 +lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
1.14 +  using mod_mult_self3 [of k n "Suc m"] by simp
1.15
1.16  lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
1.17  apply (subst mod_Suc [of m])
1.18 @@ -2004,6 +2000,10 @@
1.19  apply (auto simp add: eucl_rel_int_iff)
1.20  done
1.21
1.22 +lemma div_positive_int:
1.23 +  "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
1.24 +  using that by (simp add: divide_int_def div_positive)
1.25 +
1.26  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
1.27
1.28  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
```