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 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/lt_arith".
17 include "nat/div_and_mod.ma".
20 theorem monotonic_lt_plus_r:
21 \forall n:nat.monotonic nat lt (\lambda m.n+m).
23 elim n.simplify.assumption.
25 apply le_S_S.assumption.
28 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
31 theorem monotonic_lt_plus_l:
32 \forall n:nat.monotonic nat lt (\lambda m.m+n).
35 rewrite < sym_plus. rewrite < (sym_plus n).
36 apply lt_plus_r.assumption.
39 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
42 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
44 apply (trans_lt ? (n + q)).
45 apply lt_plus_r.assumption.
46 apply lt_plus_l.assumption.
49 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
52 rewrite > (plus_n_O q).assumption.
54 unfold lt.apply le_S_S_to_le.
56 rewrite > (plus_n_Sm q).
60 theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
61 intros.apply (lt_plus_to_lt_l n).
63 rewrite > (sym_plus q).assumption.
66 theorem le_to_lt_to_plus_lt: \forall a,b,c,d:nat.
67 a \le c \to b \lt d \to (a + b) \lt (c+d).
69 cut (a \lt c \lor a = c)
74 apply (lt_plus_r c b d).
77 | apply le_to_or_lt_eq.
84 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
85 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
88 theorem lt_times_eq_O: \forall a,b:nat.
89 O \lt a \to (a * b) = O \to b = O.
96 rewrite > (S_pred a) in H1
98 apply (eq_to_not_lt O ((S (pred a))*(S m)))
101 | apply lt_O_times_S_S
108 theorem O_lt_times_to_O_lt: \forall a,c:nat.
109 O \lt (a * c) \to O \lt a.
122 theorem monotonic_lt_times_r:
123 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
126 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
127 apply lt_plus.assumption.assumption.
130 (* a simple variant of the previus monotionic_lt_times *)
131 theorem monotonic_lt_times_variant: \forall c:nat.
132 O \lt c \to monotonic nat lt (\lambda t.(t*c)).
134 apply (increasing_to_monotonic).
139 rewrite > plus_n_O in \vdash (? % ?).
144 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
145 \def monotonic_lt_times_r.
147 theorem monotonic_lt_times_l:
148 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
151 rewrite < sym_times.rewrite < (sym_times (S m)).
152 apply lt_times_r.assumption.
155 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
156 \def monotonic_lt_times_l.
158 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
161 apply (lt_O_n_elim m H).
164 apply (lt_O_n_elim q Hcut).
165 intro.change with (O < (S m1)*(S m2)).
166 apply lt_O_times_S_S.
167 apply (ltn_to_ltO p q H1).
168 apply (trans_lt ? ((S n1)*q)).
169 apply lt_times_r.assumption.
171 apply (lt_O_n_elim q Hcut).
175 apply (ltn_to_ltO p q H2).
179 \forall n,m,p. O < n \to m < p \to n*m < n*p.
181 elim H;apply lt_times_r;assumption.
185 \forall n,m,p. O < n \to m < p \to m*n < p*n.
187 elim H;apply lt_times_l;assumption.
190 theorem lt_to_le_to_lt_times :
191 \forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
193 apply (le_to_lt_to_lt ? (n*m1))
194 [apply le_times_r.assumption
196 [assumption|assumption]
200 theorem lt_times_to_lt_l:
201 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
203 cut (p < q \lor p \nlt q).
206 absurd (p * (S n) < q * (S n)).
212 exact (decidable_lt p q).
215 theorem lt_times_n_to_lt:
216 \forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
219 [intros.apply False_ind.apply (not_le_Sn_n ? H)
220 |intros 4.apply lt_times_to_lt_l
224 theorem lt_times_to_lt_r:
225 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
227 apply (lt_times_to_lt_l n).
229 rewrite < (sym_times (S n)).
233 theorem lt_times_n_to_lt_r:
234 \forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
237 [intros.apply False_ind.apply (not_le_Sn_n ? H)
238 |intros 4.apply lt_times_to_lt_r
242 theorem nat_compare_times_l : \forall n,p,q:nat.
243 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
244 intros.apply nat_compare_elim.intro.
245 apply nat_compare_elim.
248 apply (inj_times_r n).assumption.
249 apply lt_to_not_eq. assumption.
251 apply (lt_times_to_lt_r n).assumption.
252 apply le_to_not_lt.apply lt_to_le.assumption.
253 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
254 intro.apply nat_compare_elim.intro.
256 apply (lt_times_to_lt_r n).assumption.
257 apply le_to_not_lt.apply lt_to_le.assumption.
260 apply (inj_times_r n).assumption.
261 apply lt_to_not_eq.assumption.
267 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m.
268 intros 4.apply (lt_O_n_elim m H).intros.
269 apply (lt_times_to_lt_r m1).
271 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
277 unfold lt.apply le_S_S.apply le_O_n.
280 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
282 apply (nat_case1 (n / m)).intro.
283 assumption.intros.rewrite < H2.
284 rewrite > (div_mod n m) in \vdash (? ? %).
285 apply (lt_to_le_to_lt ? ((n / m)*m)).
286 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
299 apply (trans_lt ? (S O)).
300 unfold lt. apply le_n.assumption.
304 (* general properties of functions *)
305 theorem monotonic_to_injective: \forall f:nat\to nat.
306 monotonic nat lt f \to injective nat nat f.
307 unfold injective.intros.
308 apply (nat_compare_elim x y).
309 intro.apply False_ind.apply (not_le_Sn_n (f x)).
310 rewrite > H1 in \vdash (? ? %).
311 change with (f x < f y).
314 intro.apply False_ind.apply (not_le_Sn_n (f y)).
315 rewrite < H1 in \vdash (? ? %).
316 change with (f y < f x).
320 theorem increasing_to_injective: \forall f:nat\to nat.
321 increasing f \to injective nat nat f.
322 intros.apply monotonic_to_injective.
323 apply increasing_to_monotonic.assumption.