equal
deleted
inserted
replaced
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 |] |