equal
deleted
inserted
replaced
69 lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> nat|] ==> i dvd k" |
69 lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> nat|] ==> i dvd k" |
70 by (auto simp add: divides_def mult_assoc) |
70 by (auto simp add: divides_def mult_assoc) |
71 |
71 |
72 lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k" |
72 lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k" |
73 apply (simp add: divides_def, clarify) |
73 apply (simp add: divides_def, clarify) |
74 apply (rule_tac x = "i#*k" in bexI) |
74 apply (rule_tac x = "i#*ka" in bexI) |
75 apply (simp add: mult_ac) |
75 apply (simp add: mult_ac) |
76 apply (rule mult_type) |
76 apply (rule mult_type) |
77 done |
77 done |
78 |
78 |
79 |
79 |