src/HOL/IntDiv.thy
changeset 30181 05629f28f0f7
parent 30180 6d29a873141f
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/IntDiv.thy	Sun Mar 01 10:24:57 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Sun Mar 01 12:01:57 2009 +0100
     1.3 @@ -689,9 +689,6 @@
     1.4  apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
     1.5  done
     1.6  
     1.7 -lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
     1.8 -by (simp add: zdiv_zmult1_eq)
     1.9 -
    1.10  lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
    1.11  apply (case_tac "b = 0", simp)
    1.12  apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
    1.13 @@ -717,7 +714,7 @@
    1.14    assume not0: "b \<noteq> 0"
    1.15    show "(a + c * b) div b = c + a div b"
    1.16      unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
    1.17 -      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
    1.18 +      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
    1.19  qed auto
    1.20  
    1.21  lemma posDivAlg_div_mod: