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 (* convertibility problem here *)
120 cut Or (lt p q) (Not (lt p q)).
123 absurd lt (times p (S n)) (times q (S n)).
129 exact decidable_lt p q.
132 theorem lt_times_to_lt_r:
133 \forall n,p,q:nat. lt (times (S n) p) (times(S n) q) \to lt p q.
135 apply lt_times_to_lt_l n.
137 rewrite < sym_times (S n).
141 theorem nat_compare_times_l : \forall n,p,q:nat.
142 eq compare (nat_compare p q) (nat_compare (times (S n) p) (times (S n) q)).
143 intros.apply nat_compare_elim.intro.
144 apply nat_compare_elim.
146 intro.absurd eq nat p q.
147 apply inj_times_r n.assumption.
148 apply lt_to_not_eq. assumption.
150 apply lt_times_to_lt_r n.assumption.
151 apply le_to_not_lt.apply lt_to_le.assumption.
152 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
153 intro.apply nat_compare_elim.intro.
155 apply lt_times_to_lt_r n.assumption.
156 apply le_to_not_lt.apply lt_to_le.assumption.
157 intro.absurd eq nat q p.
159 apply inj_times_r n.assumption.
160 apply lt_to_not_eq.assumption.