1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/div_and_mod_diseq".
17 include "nat/lt_arith.ma".
21 called lt_mod_m_m, is in div_and_mod.
22 Other inequalities are also in lt_arith.ma.
25 theorem lt_div_S: \forall n,m. O < m \to
28 change with (n < m +(n/m)*m).
30 rewrite > (div_mod n m H) in ⊢ (? % ?).
36 theorem le_div: \forall n,m. O < n \to m/n \le m.
38 rewrite > (div_mod m n) in \vdash (? ? %)
39 [apply (trans_le ? (m/n*n))
40 [rewrite > times_n_SO in \vdash (? % ?).
42 [apply le_n|assumption]
49 theorem le_plus_mod: \forall m,n,q. O < q \to
50 (m+n) \mod q \le m \mod q + n \mod q .
52 elim (decidable_le q (m \mod q + n \mod q))
53 [apply not_lt_to_le.intro.
54 apply (le_to_not_lt q q)
56 |apply (le_to_lt_to_lt ? (m\mod q+n\mod q))
58 |apply (trans_lt ? ((m+n)\mod q))
60 |apply lt_mod_m_m.assumption
64 |cut ((m+n)\mod q = m\mod q+n\mod q)
65 [rewrite < Hcut.apply le_n
66 |apply (div_mod_spec_to_eq2 (m+n) q ((m+n)/q) ((m+n) \mod q) (m/q + n/q))
67 [apply div_mod_spec_div_mod.
69 |apply div_mod_spec_intro
70 [apply not_le_to_lt.assumption
71 |rewrite > (div_mod n q H) in ⊢ (? ? (? ? %) ?).
73 rewrite < assoc_plus in ⊢ (? ? ? %).
75 [rewrite > (div_mod m q) in ⊢ (? ? (? % ?) ?)
76 [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
77 rewrite > distr_times_plus.
78 rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)).
80 rewrite > assoc_plus in ⊢ (? ? ? %).
95 theorem le_plus_div: \forall m,n,q. O < q \to
96 m/q + n/q \le (m+n)/q.
98 apply (le_times_to_le q)
100 |rewrite > distr_times_plus.
102 rewrite > sym_times in ⊢ (? (? ? %) ?).
103 rewrite > sym_times in ⊢ (? ? %).
104 apply (le_plus_to_le ((m+n) \mod q)).
105 rewrite > sym_plus in ⊢ (? ? %).
106 rewrite < (div_mod ? ? H).
107 rewrite > (div_mod n q H) in ⊢ (? ? (? ? %)).
108 rewrite < assoc_plus.
109 rewrite > sym_plus in ⊢ (? ? (? ? %)).
110 rewrite < assoc_plus in ⊢ (? ? %).
112 rewrite > (div_mod m q H) in ⊢ (? ? (? % ?)).
113 rewrite > assoc_plus.
121 theorem le_times_to_le_div: \forall a,b,c:nat.
122 O \lt b \to (b*c) \le a \to c \le (a /b).
125 apply (lt_times_n_to_lt b)
127 |rewrite > sym_times.
128 apply (le_to_lt_to_lt ? a)
132 rewrite > (div_mod a b) in ⊢ (? % ?)
142 theorem le_times_to_le_div2: \forall m,n,q. O < q \to
143 n \le m*q \to n/q \le m.
145 apply (le_times_to_le q ? ? H).
147 rewrite > sym_times in ⊢ (? ? %).
148 apply (le_plus_to_le (n \mod q)).
151 [apply (trans_le ? (m*q))
160 theorem lt_m_nm: \forall n,m. O < m \to S O < n \to
164 [simplify.rewrite < plus_n_O.
165 rewrite > plus_n_O in ⊢ (? % ?).
166 apply lt_plus_r.assumption
168 rewrite > plus_n_O in ⊢ (? % ?).
177 theorem lt_times_to_lt: \forall i,n,m. O < i \to
178 i * n < i * m \to n < m.
180 apply not_le_to_lt.intro.
181 apply (lt_to_not_le ? ? H1).
186 theorem lt_times_to_lt_div: \forall m,n,q. n < m*q \to n/q < m.
188 apply (lt_times_to_lt q ? ? (lt_times_to_lt_O ? ? ? H)).
190 rewrite > sym_times in ⊢ (? ? %).
191 apply (le_plus_to_le (n \mod q)).
195 [apply (trans_le ? (m*q))
199 |apply (lt_times_to_lt_O ? ? ? H)
203 theorem lt_div: \forall n,m. O < m \to S O < n \to m/n < m.
205 apply lt_times_to_lt_div.
207 apply lt_m_nm;assumption.
210 theorem le_div_plus_S: \forall m,n,q. O < q \to
211 (m+n)/q \le S(m/q + n/q).
214 apply lt_times_to_lt_div.
215 change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
217 rewrite > distr_times_plus.
219 rewrite < assoc_plus in ⊢ (? ? (? ? %)).
220 rewrite < assoc_plus.
221 rewrite > sym_plus in ⊢ (? ? (? % ?)).
222 rewrite > assoc_plus.
224 [change with (m < S(m/q)*q).
227 |rewrite > sym_times.
228 change with (n < S(n/q)*q).
234 theorem le_div_S_S_div: \forall n,m. O < m \to
235 (S n)/m \le S (n /m).
237 apply le_times_to_le_div2
240 rewrite > (div_mod n m H) in ⊢ (? (? %) ?).
249 theorem le_times_div_div_times: \forall a,n,m.O < m \to
252 apply le_times_to_le_div
254 |rewrite > sym_times.
255 rewrite > assoc_times.
257 rewrite > (div_mod n m H) in ⊢ (? ? %).
262 theorem monotonic_div: \forall n.O < n \to
263 monotonic nat le (\lambda m.div m n).
264 unfold monotonic.simplify.intros.
265 apply le_times_to_le_div
267 |apply (trans_le ? x)
268 [rewrite > sym_times.
269 rewrite > (div_mod x n H) in ⊢ (? ? %).
276 theorem le_div_times_m: \forall a,i,m. O < i \to O < m \to
277 (a * (m / i)) / m \le a / i.
279 apply (trans_le ? ((a*m/i)/m))
282 |apply le_times_div_div_times.
285 |rewrite > eq_div_div_div_times
286 [rewrite > sym_times in ⊢ (? (? ? %) ?).
287 rewrite < eq_div_div_div_times
290 |rewrite > lt_O_to_div_times
304 theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to
305 a / i \le (a * S (m / i))/m.
307 apply (trans_le ? ((a * S (m / i))/((S (m/i))*i)))
308 [rewrite < (eq_div_div_div_times ? i)
309 [rewrite > lt_O_to_div_times
316 |apply le_times_to_le_div
318 |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
319 [apply le_times_div_div_times.
320 rewrite > (times_n_O O).
325 |rewrite > sym_times.
326 apply le_times_to_le_div2
327 [rewrite > (times_n_O O).