src/HOL/Integ/IntDiv.thy
changeset 13716 73de0ef7cb25
parent 13601 fd3e3d6b37b2
child 13788 fd03c4ab89d4
equal deleted inserted replaced
13715:61bfaa892a41 13716:73de0ef7cb25
   626   thus "m mod d = 0" by auto
   626   thus "m mod d = 0" by auto
   627 qed
   627 qed
   628 
   628 
   629 declare zmod_eq_0_iff [THEN iffD1, dest!]
   629 declare zmod_eq_0_iff [THEN iffD1, dest!]
   630 
   630 
       
   631 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
       
   632 by(simp add:dvd_def zmod_eq_0_iff)
   631 
   633 
   632 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   634 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   633 
   635 
   634 lemma zadd1_lemma:
   636 lemma zadd1_lemma:
   635      "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= 0 |]  
   637      "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= 0 |]