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"