equal
deleted
inserted
replaced
128 then show ?thesis by (rule add_left_imp_eq) |
128 then show ?thesis by (rule add_left_imp_eq) |
129 qed |
129 qed |
130 |
130 |
131 lemma mod_self [simp]: "a mod a = 0" |
131 lemma mod_self [simp]: "a mod a = 0" |
132 using mod_mult_self2_is_0 [of 1] by simp |
132 using mod_mult_self2_is_0 [of 1] by simp |
133 |
|
134 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1" |
|
135 using div_mult_self2_is_id [of _ 1] by simp |
|
136 |
133 |
137 lemma div_add_self1 [simp]: |
134 lemma div_add_self1 [simp]: |
138 assumes "b \<noteq> 0" |
135 assumes "b \<noteq> 0" |
139 shows "(b + a) div b = a div b + 1" |
136 shows "(b + a) div b = a div b + 1" |
140 using assms div_mult_self1 [of b a 1] by (simp add: add.commute) |
137 using assms div_mult_self1 [of b a 1] by (simp add: add.commute) |