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.
67 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
68 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
72 theorem monotonic_lt_times_r:
73 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
76 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
77 apply lt_plus.assumption.assumption.
80 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
81 \def monotonic_lt_times_r.
83 theorem monotonic_lt_times_l:
84 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
87 rewrite < sym_times.rewrite < (sym_times (S m)).
88 apply lt_times_r.assumption.
91 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
92 \def monotonic_lt_times_l.
94 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
97 apply (lt_O_n_elim m H).
100 apply (lt_O_n_elim q Hcut).
101 intro.change with (O < (S m1)*(S m2)).
102 apply lt_O_times_S_S.
103 apply (ltn_to_ltO p q H1).
104 apply (trans_lt ? ((S n1)*q)).
105 apply lt_times_r.assumption.
107 apply (lt_O_n_elim q Hcut).
111 apply (ltn_to_ltO p q H2).
115 \forall n,m,p. O < n \to m < p \to n*m < n*p.
117 elim H;apply lt_times_r;assumption.
121 \forall n,m,p. O < n \to m < p \to m*n < p*n.
123 elim H;apply lt_times_l;assumption.
126 theorem lt_to_le_to_lt_times :
127 \forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
129 apply (le_to_lt_to_lt ? (n*m1))
130 [apply le_times_r.assumption
132 [assumption|assumption]
136 theorem lt_times_to_lt_l:
137 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
139 cut (p < q \lor p \nlt q).
142 absurd (p * (S n) < q * (S n)).
148 exact (decidable_lt p q).
151 theorem lt_times_to_lt_r:
152 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
154 apply (lt_times_to_lt_l n).
156 rewrite < (sym_times (S n)).
160 theorem nat_compare_times_l : \forall n,p,q:nat.
161 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
162 intros.apply nat_compare_elim.intro.
163 apply nat_compare_elim.
166 apply (inj_times_r n).assumption.
167 apply lt_to_not_eq. assumption.
169 apply (lt_times_to_lt_r n).assumption.
170 apply le_to_not_lt.apply lt_to_le.assumption.
171 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
172 intro.apply nat_compare_elim.intro.
174 apply (lt_times_to_lt_r n).assumption.
175 apply le_to_not_lt.apply lt_to_le.assumption.
178 apply (inj_times_r n).assumption.
179 apply lt_to_not_eq.assumption.
185 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.
186 intros 4.apply (lt_O_n_elim m H).intros.
187 apply (lt_times_to_lt_r m1).
189 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
195 unfold lt.apply le_S_S.apply le_O_n.
198 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
200 apply (nat_case1 (n / m)).intro.
201 assumption.intros.rewrite < H2.
202 rewrite > (div_mod n m) in \vdash (? ? %).
203 apply (lt_to_le_to_lt ? ((n / m)*m)).
204 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
217 apply (trans_lt ? (S O)).
218 unfold lt. apply le_n.assumption.
221 (* general properties of functions *)
222 theorem monotonic_to_injective: \forall f:nat\to nat.
223 monotonic nat lt f \to injective nat nat f.
224 unfold injective.intros.
225 apply (nat_compare_elim x y).
226 intro.apply False_ind.apply (not_le_Sn_n (f x)).
227 rewrite > H1 in \vdash (? ? %).
228 change with (f x < f y).
231 intro.apply False_ind.apply (not_le_Sn_n (f y)).
232 rewrite < H1 in \vdash (? ? %).
233 change with (f y < f x).
237 theorem increasing_to_injective: \forall f:nat\to nat.
238 increasing f \to injective nat nat f.
239 intros.apply monotonic_to_injective.
240 apply increasing_to_monotonic.assumption.