]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/arithmetics/nat.ma
67b7de50b7dfb5711e9679b502720862e49c6d03
[helm.git] / matita / matita / lib / arithmetics / nat.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "basics/relations.ma".
13
14 (* Definitions **************************************************************)
15
16 (* natural numbers *)
17
18 inductive nat : Type[0] ≝
19   | O : nat
20   | S : nat → nat.
21   
22 interpretation "Natural numbers" 'N = nat.
23
24 alias num (instance 0) = "natural number".
25
26 definition pred ≝
27  λn. match n with [ O ⇒ O | S p ⇒ p].
28
29 definition not_zero: nat → Prop ≝
30  λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
31
32 (* order relations *)
33
34 inductive le (n:nat) : nat → Prop ≝
35   | le_n : le n n
36   | le_S : ∀ m:nat. le n m → le n (S m).
37
38 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
39
40 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
41
42 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
43
44 interpretation "natural 'less than'" 'lt x y = (lt x y).
45
46 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
47
48 definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
49
50 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
51
52 definition gt: nat → nat → Prop ≝ λn,m.m<n.
53
54 interpretation "natural 'greater than'" 'gt x y = (gt x y).
55
56 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
57
58 (* abstract properties *)
59
60 definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
61
62 (* arithmetic operations *)
63
64 let rec plus n m ≝ 
65  match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
66
67 interpretation "natural plus" 'plus x y = (plus x y).
68
69 let rec times n m ≝ 
70  match n with [ O ⇒ 0 | S p ⇒ m + (times p m) ].
71
72 interpretation "natural times" 'times x y = (times x y).
73
74 let rec minus n m ≝ 
75  match n with 
76  [ O ⇒ O
77  | S p ⇒ 
78         match m with
79           [ O ⇒ S p
80     | S q ⇒ minus p q ]].
81         
82 interpretation "natural minus" 'minus x y = (minus x y).
83
84 (* Generic conclusion ******************************************************)
85
86 theorem nat_case:
87  ∀n:nat.∀P:nat → Prop. 
88   (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
89 #n #P (elim n) /2/ qed.
90
91 theorem nat_elim2 :
92  ∀R:nat → nat → Prop.
93   (∀n:nat. R O n) 
94   → (∀n:nat. R (S n) O)
95   → (∀n,m:nat. R n m → R (S n) (S m))
96   → ∀n,m:nat. R n m.
97 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
98
99 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
100 /2/ qed.
101
102 (* Equalities ***************************************************************)
103
104 theorem pred_Sn : ∀n. n = pred (S n).
105 // qed.
106
107 theorem injective_S : injective nat nat S.
108 // qed.
109
110 theorem S_pred: ∀n. 0 < n → S(pred n) = n.
111 #n #posn (cases posn) //
112 qed.
113
114 theorem plus_O_n: ∀n:nat. n = 0 + n.
115 // qed.
116
117 theorem plus_n_O: ∀n:nat. n = n + 0.
118 #n (elim n) normalize // qed.
119
120 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
121 #n (elim n) normalize // qed.
122
123 theorem commutative_plus: commutative ? plus.
124 #n (elim n) normalize // qed. 
125
126 theorem associative_plus : associative nat plus.
127 #n (elim n) normalize // qed.
128
129 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
130 // qed. 
131
132 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
133 #n (elim n) normalize /3/ qed.
134
135 theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n). 
136 /2/ qed.
137
138 theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
139 // qed.
140
141 theorem times_O_n: ∀n:nat. 0 = 0 * n.
142 // qed.
143
144 theorem times_n_O: ∀n:nat. 0 = n * 0.
145 #n (elim n) // qed.
146
147 theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
148 #n (elim n) normalize // qed.
149
150 theorem commutative_times : commutative nat times. 
151 #n (elim n) normalize // qed. 
152
153 theorem distributive_times_plus : distributive nat times plus.
154 #n (elim n) normalize // qed.
155
156 theorem distributive_times_plus_r :
157   ∀a,b,c:nat. (b+c)*a = b*a + c*a.
158 // qed. 
159
160 theorem associative_times: associative nat times.
161 #n (elim n) normalize // qed.
162
163 lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
164 // qed. 
165
166 theorem times_n_1 : ∀n:nat. n = n * 1.
167 #n // qed.
168
169 theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
170 // qed.
171
172 theorem minus_O_n: ∀n:nat.0=0-n.
173 #n (cases n) // qed.
174
175 theorem minus_n_O: ∀n:nat.n=n-0.
176 #n (cases n) // qed.
177
178 theorem minus_n_n: ∀n:nat.0=n-n.
179 #n (elim n) // qed.
180
181 theorem minus_Sn_n: ∀n:nat. S 0 = (S n)-n.
182 #n (elim n) normalize // qed.
183
184 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
185 @nat_elim2 normalize // qed.
186
187 lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
188 // qed.
189
190 (* Negated equalities *******************************************************)
191
192 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
193 /2/ qed.
194
195 theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
196 #n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
197
198 theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
199 #n (elim n) /2/ qed.
200
201 (* Atomic conclusion *******************************************************)
202
203 (* not_zero *)
204
205 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
206 #n #m #Hlt (elim Hlt) // qed.
207
208 (* le *)
209
210 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
211 #n #m #lenm (elim lenm) /2/ qed.
212
213 theorem le_O_n : ∀n:nat. 0 ≤ n.
214 #n (elim n) /2/ qed.
215
216 theorem le_n_Sn : ∀n:nat. n ≤ S n.
217 /2/ qed.
218
219 theorem transitive_le : transitive nat le.
220 #a #b #c #leab #lebc (elim lebc) /2/
221 qed.
222
223 theorem le_pred_n : ∀n:nat. pred n ≤ n.
224 #n (elim n) // qed.
225
226 theorem monotonic_pred: monotonic ? le pred.
227 #n #m #lenm (elim lenm) /2/ qed.
228
229 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
230 (* demo *)
231 /2/ qed-.
232
233 theorem monotonic_le_plus_r: 
234 ∀n:nat.monotonic nat le (λm.n + m).
235 #n #a #b (elim n) normalize //
236 #m #H #leab @le_S_S /2/ qed.
237
238 theorem monotonic_le_plus_l: 
239 ∀m:nat.monotonic nat le (λn.n + m).
240 /2/ qed.
241
242 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2 
243 → n1 + m1 ≤ n2 + m2.
244 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
245 /2/ qed.
246
247 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
248 /2/ qed. 
249
250 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
251 /2/ qed.
252
253 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
254 /2/ qed.
255
256 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
257 /2/ qed.
258
259 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
260 // qed-.
261
262 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
263 #a (elim a) normalize /3/ qed. 
264
265 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
266 /2/ qed-. 
267
268 theorem monotonic_le_times_r: 
269 ∀n:nat.monotonic nat le (λm. n * m).
270 #n #x #y #lexy (elim n) normalize//(* lento /2/*)
271 #a #lea @le_plus //
272 qed.
273
274 theorem le_times: ∀n1,n2,m1,m2:nat. 
275 n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
276 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/
277 qed.
278
279 (* interessante *)
280 theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
281 #n #m #H /2/ qed.
282
283 theorem le_times_to_le: 
284 ∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
285 #a @nat_elim2 normalize
286   [//
287   |#n #H1 #H2 
288      @(transitive_le ? (a*S n)) /2/
289   |#n #m #H #lta #le
290      @le_S_S @H /2/
291   ]
292 qed-.
293
294 theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
295 #n (elim n) // #a #Hind #m (cases m) // normalize #n/2/  
296 qed.
297
298 theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
299 #a #b #c #H @(le_plus_to_le_r … b) /2/
300 qed.
301
302 lemma lt_to_le: ∀x,y. x < y → x ≤ y.
303 /2 width=2/ qed.
304
305 lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
306 // qed-.
307
308 lemma le_x_times_x: ∀x. x ≤ x * x.
309 #x elim x -x //
310 qed.
311
312 (* lt *)
313
314 theorem transitive_lt: transitive nat lt.
315 #a #b #c #ltab #ltbc (elim ltbc) /2/
316 qed.
317
318 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
319 #n #m #p #H #H1 (elim H1) /2/ qed.
320
321 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
322 #n #m #p #H (elim H) /3/ qed.
323
324 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
325 /2/ qed.
326
327 theorem ltn_to_ltO: ∀n,m:nat. n < m → 0 < m.
328 /2/ qed.
329
330 theorem lt_O_S : ∀n:nat. O < S n.
331 /2/ qed.
332
333 theorem monotonic_lt_plus_r: 
334 ∀n:nat.monotonic nat lt (λm.n+m).
335 /2/ qed.
336
337 theorem monotonic_lt_plus_l: 
338 ∀n:nat.monotonic nat lt (λm.m+n).
339 /2/ qed.
340
341 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
342 #n #m #p #q #ltnm #ltpq
343 @(transitive_lt ? (n+q))/2/ qed.
344
345 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
346 /2/ qed.
347
348 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
349 /2/ qed-.
350
351 theorem increasing_to_monotonic: ∀f:nat → nat.
352   increasing f → monotonic nat lt f.
353 #f #incr #n #m #ltnm (elim ltnm) /2/
354 qed.
355
356 theorem monotonic_lt_times_r: 
357   ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
358 #c #posc #n #m #ltnm
359 (elim ltnm) normalize
360   [/2/ 
361   |#a #_ #lt1 @(transitive_le … lt1) //
362   ]
363 qed.
364
365 theorem monotonic_lt_times_l: 
366   ∀c:nat. 0 < c → monotonic nat lt (λt.(t*c)).
367 /2/
368 qed.
369
370 theorem lt_to_le_to_lt_times: 
371 ∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
372 #n #m #p #q #ltnm #lepq #posq
373 @(le_to_lt_to_lt ? (n*q))
374   [@monotonic_le_times_r //
375   |@monotonic_lt_times_l //
376   ]
377 qed.
378
379 theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
380 #n #m #p #q #ltnm #ltpq @lt_to_le_to_lt_times/2/
381 qed.
382
383 theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
384 #a #b #c #H @le_plus_to_minus_r //
385 qed.
386
387 lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n).
388 /2 width=1/ qed.
389
390 theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
391 (* demo *)
392 /2/ qed-.
393
394 (* not le, lt *)
395
396 theorem not_le_Sn_O: ∀ n:nat. S n ≰ 0.
397 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
398
399 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
400 /3/ qed.
401
402 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
403 /3/ qed.
404
405 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
406 #n (elim n) /2/ qed.
407
408 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
409 #n #m #Hltnm (elim Hltnm) /3/ qed.
410
411 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
412 @nat_elim2 #n
413  [#abs @False_ind /2/
414  |/2/
415  |#m #Hind #HnotleSS @le_S_S @Hind /2/ 
416  ]
417 qed.
418
419 (* not lt, le *)
420
421 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
422 #n #m #H @le_S_S_to_le @not_le_to_lt /2/ qed.
423
424 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
425 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
426
427 (* Compound conclusion ******************************************************)
428
429 theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
430 @nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
431 qed. 
432
433 theorem decidable_le: ∀n,m. decidable (n≤m).
434 @nat_elim2 #n /2/ #m * /3/ qed.
435
436 theorem decidable_lt: ∀n,m. decidable (n < m).
437 #n #m @decidable_le  qed.
438
439 theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
440 #n #m #lenm (elim lenm) /3/ qed.
441
442 theorem increasing_to_le2: ∀f:nat → nat. increasing f → 
443   ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
444 #f #incr #m #lem (elim lem)
445   [@(ex_intro ? ? O) /2/
446   |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
447     [@(ex_intro ? ? a) % /2/ 
448     |@(ex_intro ? ? (S a)) % //
449     ]
450   ]
451 qed.
452
453 lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
454 /3/ qed-.
455
456 lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
457 /3/ qed-.
458
459 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
460 #m #n elim (decidable_lt m n) /2/ /3/
461 qed-.
462
463 lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
464 #m #n elim (decidable_le m n) /2/ /4/
465 qed-.
466
467 (* More general conclusion **************************************************)
468
469 theorem nat_ind_plus: ∀R:predicate nat.
470                       R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
471 /3 by nat_ind/ qed-.
472
473 theorem lt_O_n_elim: ∀n:nat. 0 < n → 
474   ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
475 #n (elim n) // #abs @False_ind /2/ @absurd
476 qed.
477
478 theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
479 #n (cases n) // #a #abs @False_ind /2/ qed. 
480
481 theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m → 
482 ∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
483 #n #m #Hle #P (elim Hle) /3/ qed.
484
485 theorem nat_elim1 : ∀n:nat.∀P:nat → Prop. 
486 (∀m.(∀p. p < m → P p) → P m) → P n.
487 #n #P #H 
488 cut (∀q:nat. q ≤ n → P q) /2/
489 (elim n) 
490  [#q #HleO (* applica male *) 
491     @(le_n_O_elim ? HleO)
492     @H #p #ltpO @False_ind /2/ (* 3 *)
493  |#p #Hind #q #HleS 
494     @H #a #lta @Hind @le_S_S_to_le /2/
495  ]
496 qed.
497
498 lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
499              (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
500 #A #f #P #H #a
501 cut (∀n,a. f a = n → P a) /2 width=3/ -a
502 #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto very slow (274s) without #n *)
503 qed-.
504
505 (* More negated equalities **************************************************)
506
507 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
508 #n #m #H @not_to_not /2/ qed.
509
510 (* More equalities **********************************************************)
511
512 theorem le_n_O_to_eq : ∀n:nat. n ≤ 0 → 0=n.
513 #n (cases n) // #a  #abs @False_ind /2/ qed.
514
515 theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
516 @nat_elim2 /4 by le_n_O_to_eq, monotonic_pred, eq_f, sym_eq/
517 qed. 
518
519 theorem increasing_to_injective: ∀f:nat → nat.
520   increasing f → injective nat nat f.
521 #f #incr #n #m cases(decidable_le n m)
522   [#lenm cases(le_to_or_lt_eq … lenm) //
523    #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq 
524    @increasing_to_monotonic //
525   |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq 
526    @lt_to_not_eq @increasing_to_monotonic /2/
527   ]
528 qed.
529
530 theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
531 (* qualcosa da capire qui 
532 #n #m #lenm nelim lenm napplyS refl_eq. *)
533 @nat_elim2 
534   [//
535   |#n #abs @False_ind /2/ 
536   |#n #m #Hind #c applyS Hind /2/
537   ]
538 qed.
539
540 theorem plus_minus:
541 ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
542 @nat_elim2 
543   [//
544   |#n #p #abs @False_ind /2/
545   |normalize/3/
546   ]
547 qed.
548
549 theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
550 /2/ qed.
551
552 theorem plus_minus_m_m: ∀n,m:nat.
553   m ≤ n → n = (n-m)+m.
554 #n #m #lemn @sym_eq /2/ qed.
555
556 theorem minus_to_plus :∀n,m,p:nat.
557   m ≤ n → n-m = p → n = m+p.
558 #n #m #p #lemn #eqp (applyS plus_minus_m_m) //
559 qed.
560
561 theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
562 #n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
563 qed.
564
565 theorem minus_pred_pred : ∀n,m:nat. O < n → O < m → 
566 pred n - pred m = n - m.
567 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
568 qed.
569
570 theorem plus_minus_commutative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
571 /2 by plus_minus/ qed.
572
573 (* More atomic conclusion ***************************************************)
574
575 (* le *)
576
577 theorem le_n_fn: ∀f:nat → nat. 
578   increasing f → ∀n:nat. n ≤ f n.
579 #f #incr #n (elim n) /2/
580 qed-.
581
582 theorem monotonic_le_minus_l: 
583 ∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
584 @nat_elim2 #p #q
585   [#lePO @(le_n_O_elim ? lePO) //
586   |//
587   |#Hind #n (cases n) // #a #leSS @Hind /2/
588   ]
589 qed.
590
591 theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
592 #n #m #p #lep @transitive_le
593   [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
594 qed.
595
596 theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
597 #a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
598 qed.
599
600 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
601 #n #m #p #lep /2/ qed.
602
603 theorem monotonic_le_minus_r: 
604 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
605 #p #q #n #lepq @le_plus_to_minus
606 @(transitive_le … (le_plus_minus_m_m ? q)) /2/
607 qed.
608
609 theorem increasing_to_le: ∀f:nat → nat. 
610   increasing f → ∀m:nat.∃i.m ≤ f i.
611 #f #incr #m (elim m) /2/#n * #a #lenfa
612 @(ex_intro ?? (S a)) /2/
613 qed.
614
615 (* thus is le_plus
616 lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
617 #x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
618 *)
619
620 lemma minus_le: ∀x,y. x - y ≤ x.
621 /2 width=1/ qed.
622
623 (* lt *)
624
625 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
626 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
627 #Heq @not_le_to_lt /2/ qed-.
628
629 theorem lt_times_n_to_lt_l: 
630 ∀n,p,q:nat. p*n < q*n → p < q.
631 #n #p #q #Hlt (elim (decidable_lt p q)) //
632 #nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
633 applyS monotonic_le_times_r /2/
634 qed.
635
636 theorem lt_times_n_to_lt_r: 
637 ∀n,p,q:nat. n*p < n*q → p < q.
638 /2/ qed-.
639
640 theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
641 #a #b #c #H @not_le_to_lt 
642 @(not_to_not … (lt_to_not_le …H)) /2/
643 qed.
644
645 theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
646 #a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
647 @lt_to_not_le //
648 qed.
649
650 theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
651 #n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
652 qed.
653
654 theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
655 #p #q #n #H1 #H2
656 @lt_plus_to_minus_r <plus_minus_m_m //
657 qed.
658
659 (* More compound conclusion *************************************************)
660
661 lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
662 * /2 width=1/ #x * /2 width=1/ #y normalize #H 
663 lapply (minus_le x y) <H -H #H
664 elim (not_le_Sn_n x) #H0 elim (H0 ?) //
665 qed-.
666
667 (* Still more equalities ****************************************************)
668
669 theorem eq_minus_O: ∀n,m:nat.
670   n ≤ m → n-m = O.
671 #n #m #lenm @(le_n_O_elim (n-m)) /2/
672 qed.
673
674 theorem distributive_times_minus: distributive ? times minus.
675 #a #b #c
676 (cases (decidable_lt b c)) #Hbc
677  [> eq_minus_O [2:/2/] >eq_minus_O // 
678   @monotonic_le_times_r /2/
679  |@sym_eq (applyS plus_to_minus) <distributive_times_plus 
680   @eq_f (applyS plus_minus_m_m) /2/
681 qed.
682
683 theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
684 #n #m #p 
685 cases (decidable_le (m+p) n) #Hlt
686   [@plus_to_minus @plus_to_minus <associative_plus
687    @minus_to_plus //
688   |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
689    #H >eq_minus_O /2/ (* >eq_minus_O // *) 
690   ]
691 qed.
692
693 theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
694   p+(n-m) = n-(m-p).
695 #n #m #p #lepm #lemn
696 @sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
697 <commutative_plus <plus_minus_m_m //
698 qed.
699
700 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
701 /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
702
703 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
704 #b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
705 qed.
706
707 lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
708 /2 width=1/ qed.
709
710 lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
711 // qed.
712
713 (* Stilll more atomic conclusion ********************************************)
714
715 (* le *)
716
717 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
718 #m1 #m2 #H #n1 #n2 >commutative_plus
719 #H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
720 #H #_ @(transitive_le … H) /2 width=1/
721 qed-. 
722
723 (*********************** boolean arithmetics ********************) 
724
725 include "basics/bool.ma".
726
727 let rec eqb n m ≝ 
728 match n with 
729   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
730   | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
731   ].
732
733 theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
734 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 
735 @nat_elim2 
736   [#n (cases n) normalize /3/ 
737   |normalize /3/
738   |normalize /4/ 
739   ] 
740 qed.
741
742 theorem eqb_n_n: ∀n. eqb n n = true.
743 #n (elim n) normalize // qed. 
744
745 theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
746 #n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
747
748 theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
749 #n #m @(eqb_elim n m) /2/ qed.
750
751 theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
752 // qed.
753
754 theorem not_eq_to_eqb_false: ∀n,m:nat.
755   n ≠  m → eqb n m = false.
756 #n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
757
758 let rec leb n m ≝ 
759 match n with 
760     [ O ⇒ true
761     | (S p) ⇒
762         match m with 
763         [ O ⇒ false
764               | (S q) ⇒ leb p q]].
765
766 theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. 
767 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
768 @nat_elim2 normalize
769   [/2/
770   |/3/
771   |#n #m #Hind #P #Pt #Pf @Hind
772     [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
773   ]
774 qed.
775
776 theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
777 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
778
779 theorem leb_false_to_not_le:∀n,m.
780   leb n m = false → n ≰ m.
781 #n #m @leb_elim // #_ #abs @False_ind /2/ qed.
782
783 theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
784 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
785
786 theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
787 #n #m @leb_elim // #H #H1 @False_ind /2/ qed.
788
789 theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
790 /3/ qed.
791
792 (* min e max *)
793 definition min: nat →nat →nat ≝
794 λn.λm. if leb n m then n else m.
795
796 definition max: nat →nat →nat ≝
797 λn.λm. if leb n m then m else n.
798
799 lemma commutative_min: commutative ? min.
800 #n #m normalize @leb_elim 
801   [@leb_elim normalize /2/
802   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
803   ] qed.
804
805 lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
806 #i #n #m normalize @leb_elim normalize /2/ qed. 
807
808 lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
809 /2/ qed-.
810
811 lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
812 #i #n #m #lein #leim normalize (cases (leb n m)) 
813 normalize // qed.
814
815 lemma commutative_max: commutative ? max.
816 #n #m normalize @leb_elim 
817   [@leb_elim normalize /2/
818   |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
819   ] qed.
820
821 lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
822 #i #n #m normalize @leb_elim normalize /2/ qed. 
823
824 lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
825 /2/ qed-.
826
827 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
828 #i #n #m #leni #lemi normalize (cases (leb n m)) 
829 normalize // qed.