96 using mod_mult_self2_is_0 [of 1] by simp |
96 using mod_mult_self2_is_0 [of 1] by simp |
97 |
97 |
98 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1" |
98 lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1" |
99 using div_mult_self2_is_id [of _ 1] by simp |
99 using div_mult_self2_is_id [of _ 1] by simp |
100 |
100 |
101 lemma div_add_self1: |
101 lemma div_add_self1 [simp]: |
102 assumes "b \<noteq> 0" |
102 assumes "b \<noteq> 0" |
103 shows "(b + a) div b = a div b + 1" |
103 shows "(b + a) div b = a div b + 1" |
104 using assms div_mult_self1 [of b a 1] by (simp add: add_commute) |
104 using assms div_mult_self1 [of b a 1] by (simp add: add_commute) |
105 |
105 |
106 lemma div_add_self2: |
106 lemma div_add_self2 [simp]: |
107 assumes "b \<noteq> 0" |
107 assumes "b \<noteq> 0" |
108 shows "(a + b) div b = a div b + 1" |
108 shows "(a + b) div b = a div b + 1" |
109 using assms div_add_self1 [of b a] by (simp add: add_commute) |
109 using assms div_add_self1 [of b a] by (simp add: add_commute) |
110 |
110 |
111 lemma mod_add_self1: |
111 lemma mod_add_self1 [simp]: |
112 "(b + a) mod b = a mod b" |
112 "(b + a) mod b = a mod b" |
113 using mod_mult_self1 [of a 1 b] by (simp add: add_commute) |
113 using mod_mult_self1 [of a 1 b] by (simp add: add_commute) |
114 |
114 |
115 lemma mod_add_self2: |
115 lemma mod_add_self2 [simp]: |
116 "(a + b) mod b = a mod b" |
116 "(a + b) mod b = a mod b" |
117 using mod_mult_self1 [of a 1 b] by simp |
117 using mod_mult_self1 [of a 1 b] by simp |
118 |
118 |
119 lemma mod_div_decomp: |
119 lemma mod_div_decomp: |
120 fixes a b |
120 fixes a b |