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.plus n m).
23 elim n.simplify.assumption.
25 apply le_S_S.assumption.
28 variant lt_plus_r: \forall n,p,q:nat. lt p q \to lt (plus n p) (plus n q) \def
31 theorem monotonic_lt_plus_l:
32 \forall n:nat.monotonic nat lt (\lambda m.plus m n).
33 change with \forall n,p,q:nat. lt p q \to lt (plus p n) (plus q 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. lt p q \to lt (plus p n) (plus q n) \def
42 theorem lt_plus: \forall n,m,p,q:nat. lt n m \to lt p q \to lt (plus n p) (plus m q).
44 apply trans_lt ? (plus 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. lt (plus p n) (plus q n) \to lt p q.
52 rewrite > plus_n_O q.assumption.
54 simplify.apply le_S_S_to_le.
56 rewrite > plus_n_Sm q.
60 theorem lt_plus_to_lt_r :\forall n,p,q:nat. lt (plus n p) (plus n q) \to lt 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.lt O (times (S n) (S m)).
68 intros.simplify.apply le_S_S.apply le_O_n.
72 theorem monotonic_lt_times_r:
73 \forall n:nat.monotonic nat lt (\lambda m.times (S n) m).
74 change with \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q).
76 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
77 change with lt (plus p (times (S n1) p)) (plus q (times (S n1) q)).
78 apply lt_plus.assumption.assumption.
81 theorem lt_times_r: \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q)
82 \def monotonic_lt_times_r.
84 theorem monotonic_lt_times_l:
85 \forall m:nat.monotonic nat lt (\lambda n.times n (S m)).
87 \forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n)).
89 rewrite < sym_times.rewrite < sym_times (S n).
90 apply lt_times_r.assumption.
93 variant lt_times_l: \forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n))
94 \def monotonic_lt_times_l.
96 theorem lt_times:\forall n,m,p,q:nat. lt n m \to lt p q \to lt (times n p) (times m q).
99 apply lt_O_n_elim m H.
102 apply lt_O_n_elim q Hcut.
103 intro.change with lt O (times (S m1) (S m2)).
104 apply lt_O_times_S_S.
105 apply ltn_to_ltO p q H1.
106 apply trans_lt ? (times (S n1) q).
107 apply lt_times_r.assumption.
109 apply lt_O_n_elim q Hcut.
113 apply ltn_to_ltO p q H2.
116 theorem lt_times_to_lt_l:
117 \forall n,p,q:nat. lt (times p (S n)) (times q (S n)) \to lt p q.
119 cut Or (lt p q) (Not (lt p q)).
122 absurd lt (times p (S n)) (times q (S n)).
128 exact decidable_lt p q.
131 theorem lt_times_to_lt_r:
132 \forall n,p,q:nat. lt (times (S n) p) (times(S n) q) \to lt p q.
134 apply lt_times_to_lt_l n.
136 rewrite < sym_times (S n).
140 theorem nat_compare_times_l : \forall n,p,q:nat.
141 eq compare (nat_compare p q) (nat_compare (times (S n) p) (times (S n) q)).
142 intros.apply nat_compare_elim.intro.
143 apply nat_compare_elim.
145 intro.absurd eq nat p q.
146 apply inj_times_r n.assumption.
147 apply lt_to_not_eq. assumption.
149 apply lt_times_to_lt_r n.assumption.
150 apply le_to_not_lt.apply lt_to_le.assumption.
151 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
152 intro.apply nat_compare_elim.intro.
154 apply lt_times_to_lt_r n.assumption.
155 apply le_to_not_lt.apply lt_to_le.assumption.
156 intro.absurd eq nat q p.
158 apply inj_times_r n.assumption.
159 apply lt_to_not_eq.assumption.
165 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to mod n m = O \to O < div n m.
166 intros 4.apply lt_O_n_elim m H.intros.
167 apply lt_times_to_lt_r m1.
169 rewrite > plus_n_O ((S m1)*(div n (S m1))).
175 simplify.apply le_S_S.apply le_O_n.
178 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to div n m \lt n.
180 apply nat_case1 (div n m).intro.
181 assumption.intros.rewrite < H2.
182 rewrite > (div_mod n m) in \vdash (? ? %).
183 apply lt_to_le_to_lt ? ((div n m)*m).
184 apply lt_to_le_to_lt ? ((div n m)*(S (S O))).
197 apply trans_lt ? (S O).
198 simplify. apply le_n.assumption.
201 (* general properties of functions *)
202 theorem monotonic_to_injective: \forall f:nat\to nat.
203 monotonic nat lt f \to injective nat nat f.
205 apply nat_compare_elim x y.
206 intro.apply False_ind.apply not_le_Sn_n (f x).
207 rewrite > H1 in \vdash (? ? %).apply H.apply H2.
209 intro.apply False_ind.apply not_le_Sn_n (f y).
210 rewrite < H1 in \vdash (? ? %).apply H.apply H2.
213 theorem increasing_to_injective: \forall f:nat\to nat.
214 increasing f \to injective nat nat f.
215 intros.apply monotonic_to_injective.
216 apply increasing_to_monotonic.assumption.