]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/nlibrary/arithmetics/Z.ma
Large commit:
[helm.git] / matita / matita / nlibrary / arithmetics / Z.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "arithmetics/nat.ma".
16
17 ninductive Z : Type ≝
18   OZ : Z
19 | pos : nat → Z
20 | neg : nat → Z.
21
22 interpretation "Integers" 'Z = Z.
23
24 ndefinition Z_of_nat ≝
25 λn. match n with
26 [ O ⇒ OZ 
27 | S n ⇒ pos n].
28
29 ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.
30
31 ndefinition neg_Z_of_nat \def
32 λn. match n with
33 [ O ⇒ OZ 
34 | S n ⇒ neg n].
35
36 nlemma pos_n_eq_S_n : ∀n : nat.pos n = S n.
37 //.
38 nqed.
39
40 ndefinition abs ≝
41 λz.match z with 
42 [ OZ ⇒ O
43 | pos n ⇒ S n
44 | neg n ⇒ S n].
45
46 ndefinition OZ_test ≝
47 λz.match z with 
48 [ OZ ⇒ true
49 | pos _ ⇒ false
50 | neg _ ⇒ false].
51
52 ntheorem OZ_test_to_Prop : ∀z:Z.
53   match OZ_test z with
54   [true ⇒ z=OZ 
55   |false ⇒ z ≠ OZ].
56 #z;ncases z
57 ##[napply refl
58 ##|##*:#z1;napply nmk;#H;ndestruct]
59 nqed.
60
61 (* discrimination *)
62 ntheorem injective_pos: injective nat Z pos.
63 #n;#m;#H;ndestruct;//;
64 nqed.
65
66 (* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
67 \def injective_pos. *)
68
69 ntheorem injective_neg: injective nat Z neg.
70 #n;#m;#H;ndestruct;//;
71 nqed.
72
73 (* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
74 \def injective_neg. *)
75
76 ntheorem not_eq_OZ_pos: ∀n:nat. OZ ≠ pos n.
77 #n;napply nmk;#H;ndestruct;
78 nqed.
79
80 ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n.
81 #n;napply nmk;#H;ndestruct;
82 nqed.
83
84 ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m.
85 #n;#m;napply nmk;#H;ndestruct;
86 nqed.
87
88 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
89 #x;#y;ncases x;
90 ##[ncases y;
91    ##[@;//
92    ##|##*:#n;@2;napply nmk;#H;ndestruct]
93 ##|#n;ncases y;
94    ##[@2;napply nmk;#H;ndestruct;
95    ##|#m;ncases (decidable_eq_nat n m);#H;
96       ##[nrewrite > H;@;//
97       ##|@2;napply nmk;#H2;nelim H;
98          (* bug if you don't introduce H3 *)#H3;ndestruct;
99          napply H3;@]
100    ##|#m;@2;napply nmk;#H;ndestruct]
101 ##|#n;ncases y;
102    ##[@2;napply nmk;#H;ndestruct;
103    ##|#m;@2;napply nmk;#H;ndestruct
104    ##|#m;ncases (decidable_eq_nat n m);#H;
105       ##[nrewrite > H;@;//
106       ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct;
107          napply H3;@]##]##]
108 nqed.
109
110 ndefinition Zsucc ≝
111 λz. match z with
112 [ OZ ⇒ pos O
113 | pos n ⇒ pos (S n)
114 | neg n ⇒
115           match n with
116           [ O ⇒ OZ
117           | S p ⇒ neg p]].
118
119 ndefinition Zpred ≝
120 λz. match z with
121 [ OZ ⇒ neg O
122 | pos n ⇒
123           match n with
124           [ O ⇒ OZ
125           | S p ⇒ pos p]
126 | neg n ⇒ neg (S n)].
127
128 ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
129 #z;ncases z;
130 ##[##1,2://
131 ##|#n;ncases n;//]
132 nqed.
133
134 ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
135 #z;ncases z
136 ##[##2:#n;ncases n;//
137 ##|##*://]
138 nqed.
139
140 ndefinition Zle : Z → Z → Prop ≝
141 λx,y:Z.
142   match x with
143   [ OZ ⇒ 
144     match y with 
145     [ OZ ⇒ True
146     | pos m ⇒ True
147     | neg m ⇒ False ]
148   | pos n ⇒
149     match y with 
150     [ OZ ⇒ False
151     | pos m ⇒ n ≤ m
152     | neg m ⇒ False ]
153   | neg n ⇒
154     match y with 
155     [ OZ ⇒ True
156     | pos m ⇒ True
157     | neg m ⇒ m ≤ n ]].
158
159 interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
160 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
161
162 ndefinition Zlt : Z → Z → Prop ≝
163 λx,y:Z.
164   match x with
165   [ OZ ⇒
166     match y with 
167     [ OZ ⇒ False
168     | pos m ⇒ True
169     | neg m ⇒ False ]
170   | pos n ⇒
171     match y with 
172     [ OZ ⇒ False
173     | pos m ⇒ n<m
174     | neg m ⇒ False ]
175   | neg n ⇒
176     match y with 
177     [ OZ ⇒ True
178     | pos m ⇒ True
179     | neg m ⇒ m<n ]].
180     
181 interpretation "integer 'less than'" 'lt x y = (Zlt x y).
182 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
183
184 ntheorem irreflexive_Zlt: irreflexive Z Zlt.
185 #x;ncases x
186 ##[napply nmk;//
187 ##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
188 nqed.
189
190 (* transitivity *)
191 ntheorem transitive_Zle : transitive Z Zle.
192 #x;#y;#z;ncases x
193 ##[ncases y
194    ##[//
195    ##|##*:#n;ncases z;//]
196 ##|#n;ncases y
197    ##[#H;ncases H
198    ##|(*##*:#m;#Hl;ncases z;//;*)
199       #m;#Hl;ncases z;//;#p;#Hr;
200       napply (transitive_le n m p);//; (* XXX: auto??? *)
201    ##|#m;#Hl;ncases Hl]
202 ##|#n;ncases y
203    ##[#Hl;ncases z
204       ##[##1,2://
205       ##|#m;#Hr;ncases Hr]
206    ##|#m;#Hl;ncases z;
207       ##[##1,2://
208       ##|#p;#Hr;ncases Hr]
209    ##|#m;#Hl;ncases z;//;#p;#Hr;
210       napply (transitive_le p m n);//; (* XXX: auto??? *) ##]
211 nqed.
212
213 (* variant trans_Zle: transitive Z Zle
214 \def transitive_Zle.*)
215
216 ntheorem transitive_Zlt: transitive Z Zlt.
217 #x;#y;#z;ncases x
218 ##[ncases y
219    ##[//
220    ##|#n;ncases z
221       ##[#_;#Hr;ncases Hr
222       ##|//
223       ##|#m;#_;#Hr;ncases Hr]
224    ##|#n;#Hl;ncases Hl]
225 ##|#n;ncases y
226    ##[#Hl;ncases Hl
227    ##|#m;ncases z
228       ##[//
229       ##|#p;napply transitive_lt (* XXX: auto??? *) 
230       ##|//##]
231    ##|#m;#Hl;ncases Hl]
232 ##|#n;ncases y
233    ##[ncases z;
234       ##[##1,2://
235       ##|#m;#_;#Hr;ncases Hr]
236    ##|#m;ncases z;
237       ##[##1,2://
238       ##|#p;#_;#Hr;ncases Hr]
239    ##|#m;ncases z
240       ##[##1,2://
241       ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]
242    ##]
243 ##]
244 nqed.     
245
246 (* variant trans_Zlt: transitive Z Zlt
247 \def transitive_Zlt.
248 theorem irrefl_Zlt: irreflexive Z Zlt
249 \def irreflexive_Zlt.*)
250
251 ntheorem Zlt_neg_neg_to_lt: 
252   ∀n,m:nat. neg n < neg m → m < n.
253 //;
254 nqed.
255
256 ntheorem lt_to_Zlt_neg_neg: ∀n,m:nat.m < n → neg n < neg m. 
257 //;
258 nqed.
259
260 ntheorem Zlt_pos_pos_to_lt: 
261   ∀n,m:nat. pos n < pos m → n < m.
262 //;
263 nqed.
264
265 ntheorem lt_to_Zlt_pos_pos: ∀n,m:nat.n < m → pos n < pos m. 
266 //;
267 nqed.
268
269 ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
270 #x;#y;ncases x
271 ##[ncases y
272    ##[#H;ncases H
273    ##|//;
274    ##|#p;#H;ncases H]
275 ##|#n;ncases y
276    ##[#H;ncases H
277    ##|#p;nnormalize;//
278    ##|#p;#H;ncases H]
279 ##|#n;ncases y
280    ##[##1,2:ncases n;//
281    ##|#p;ncases n;nnormalize;
282       ##[#H;nelim (not_le_Sn_O p);#H2;napply H2;//; (* XXX: auto? *)
283       ##|#m;napply le_S_S_to_le (* XXX: auto? *)]
284    ##]
285 ##]
286 nqed.
287
288 (*** COMPARE ***)
289
290 (* boolean equality *)
291 ndefinition eqZb : Z → Z → bool ≝
292 λx,y:Z.
293   match x with
294   [ OZ ⇒
295       match y with
296         [ OZ ⇒ true
297         | pos q ⇒ false
298         | neg q ⇒ false]
299   | pos p ⇒
300       match y with
301         [ OZ ⇒ false
302         | pos q ⇒ eqb p q
303         | neg q ⇒ false]     
304   | neg p ⇒
305       match y with
306         [ OZ ⇒ false
307         | pos q ⇒ false
308         | neg q ⇒ eqb p q]].
309
310 ntheorem eqZb_to_Prop: 
311   ∀x,y:Z. 
312     match eqZb x y with
313     [ true ⇒ x=y
314     | false ⇒ x ≠ y].
315 #x;#y;ncases x
316 ##[ncases y;
317    ##[//
318    ##|napply not_eq_OZ_pos (* XXX: auto? *)
319    ##|napply not_eq_OZ_neg (* XXX: auto? *)]
320 ##|#n;ncases y;
321    ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/;
322    ##|#m;napply eqb_elim;
323       ##[//
324       ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/]
325    ##|#m;napply not_eq_pos_neg]
326 ##|#n;ncases y
327    ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/;
328    ##|#m;napply nmk;#H;ndestruct
329    ##|#m;napply eqb_elim;
330       ##[//
331       ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/]
332    ##]
333 ##]
334 nqed.
335
336 ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
337   (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
338 #x;#y;#P;#HP1;#HP2;
339 ncut 
340 (match (eqZb x y) with
341 [ true ⇒ x=y
342 | false ⇒ x ≠ y] → P (eqZb x y))
343 ##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)
344    ##[napply HP1
345    ##|napply HP2]
346 ##|#Hcut;napply Hcut;napply eqZb_to_Prop]
347 nqed.
348
349 ndefinition Z_compare : Z → Z → compare ≝
350 λx,y:Z.
351   match x with
352   [ OZ ⇒
353     match y with 
354     [ OZ ⇒ EQ
355     | pos m ⇒ LT
356     | neg m ⇒ GT ]
357   | pos n ⇒
358     match y with 
359     [ OZ ⇒ GT
360     | pos m ⇒ nat_compare n m
361     | neg m ⇒ GT]
362   | neg n ⇒ 
363     match y with 
364     [ OZ ⇒ LT
365     | pos m ⇒ LT
366     | neg m ⇒ nat_compare m n ]].
367
368 ntheorem Z_compare_to_Prop : 
369 ∀x,y:Z. match (Z_compare x y) with
370 [ LT ⇒ x < y
371 | EQ ⇒ x=y
372 | GT ⇒ y < x]. 
373 #x;#y;nelim x
374 ##[nelim y;//;
375 ##|nelim y
376    ##[##1,3://
377    ##|#n;#m;nnormalize;
378       ncut (match (nat_compare m n) with
379       [ LT ⇒ m < n
380       | EQ ⇒ m = n
381       | GT ⇒ n < m ] →
382       match (nat_compare m n) with
383       [ LT ⇒ S m  ≤ n
384       | EQ ⇒ pos m = pos n
385       | GT ⇒ S n  ≤ m])
386       ##[ncases (nat_compare m n);//
387       ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
388    ##]
389 ##|nelim y
390    ##[#n;//
391    ##|nnormalize;//
392    ##|nnormalize;#n;#m;
393       ncut (match (nat_compare n m) with
394         [ LT ⇒ n < m
395         | EQ ⇒ n = m
396         | GT ⇒ m < n] →
397       match (nat_compare n m) with
398       [ LT ⇒ S n ≤ m
399       | EQ ⇒ neg m = neg n
400       | GT ⇒ S m ≤ n])
401       ##[ncases (nat_compare n m);//
402       ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
403    ##]
404 ##]
405 nqed.
406
407 ndefinition Zplus : Z → Z → Z ≝
408   λx,y. match x with
409     [ OZ ⇒ y
410     | pos m ⇒
411         match y with
412          [ OZ ⇒ x
413          | pos n ⇒ (pos (pred ((S m)+(S n))))
414          | neg n ⇒ 
415               match nat_compare m n with
416                 [ LT ⇒ (neg (pred (n-m)))
417                 | EQ ⇒ OZ
418                 | GT ⇒ (pos (pred (m-n)))] ]
419     | neg m ⇒
420         match y with
421          [ OZ ⇒ x
422          | pos n ⇒
423               match nat_compare m n with
424                 [ LT ⇒ (pos (pred (n-m)))
425                 | EQ ⇒ OZ
426                 | GT ⇒ (neg (pred (m-n)))]     
427          | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
428
429 interpretation "integer plus" 'plus x y = (Zplus x y).
430
431 ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
432 #n;#m;ncases n
433 ##[//
434 ##|#p;ncases m
435    ##[nnormalize;//
436    ##|//]
437 nqed.
438
439 ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
440 #z;ncases z;//;
441 nqed.
442
443 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
444
445 ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.
446 #x;#y;ncases x;
447 ##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//
448 ##|#p;ncases y
449    ##[//
450    ##|nnormalize;//
451    ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
452       ncases (nat_compare q p);//]
453 ##|#p;ncases y
454    ##[//;
455    ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
456       ncases (nat_compare q p);//
457    ##|nnormalize;//]
458 ##]
459 nqed.
460
461 ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg O)+z.
462 #z;ncases z
463 ##[//
464 ##|##*:#n;ncases n;//]
465 nqed.
466
467 ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos O)+z.
468 #z;ncases z
469 ##[//
470 ##|##*:#n;ncases n;//]
471 nqed.
472
473 ntheorem Zplus_pos_pos:
474   ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
475 #n;#m;ncases n
476 ##[ncases m;//
477 ##|#p;ncases m
478    ##[nnormalize;
479       nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_O ?); (* XXX yet again *)
480       //
481    ##|#q;nnormalize;nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_Sm ??);//]
482 ##]
483 nqed.
484
485 ntheorem Zplus_pos_neg:
486   ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
487 //;
488 nqed.
489
490 ntheorem Zplus_neg_pos :
491   ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
492 #n;#m;ncases n;ncases m;//;
493 nqed.
494
495 ntheorem Zplus_neg_neg:
496   ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
497 #n;#m;ncases n
498 ##[ncases m;//
499 ##|#p;ncases m;nnormalize;
500    ##[nrewrite > (plus_n_Sm ??);//
501    ##|#q;nrewrite > (plus_n_Sm ??);//]
502 ##]
503 nqed.
504
505 ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
506 #x;#y;ncases x
507 ##[ncases y
508    ##[//
509    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
510    ##|//]
511 ##|ncases y;//
512 ##|ncases y
513    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
514       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
515    ##|##*://]
516 nqed.
517
518 ntheorem Zplus_Zsucc_pos_pos : 
519   ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
520 //;
521 nqed.
522
523 ntheorem Zplus_Zsucc_pos_neg: 
524   ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
525 #n;#m;
526 napply (nat_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
527 ##[#n1;nelim n1
528    ##[//
529    ##|#n2;#IH;nelim n2;//]
530 ##|//
531 ##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nelim IH;//]
532 nqed.
533
534 ntheorem Zplus_Zsucc_neg_neg : 
535   ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
536 #n;#m;
537 napply (nat_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
538 ##[#n1;nelim n1
539    ##[//
540    ##|#n2;#IH;nelim n2;//]
541 ##|##*://]
542 nqed.
543
544 ntheorem Zplus_Zsucc_neg_pos: 
545   ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
546 #n;#m;
547 napply (nat_elim2 (λn,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)))
548 ##[#n1;nelim n1
549    ##[//
550    ##|#n2;#IH;nelim n2;//]
551 ##|//
552 ##|#n1;#m1;#IH;nrewrite < IH;nrewrite < (Zplus_neg_pos ? (S m1));//]
553 nqed.
554
555 ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
556 #x;#y;ncases x
557 ##[ncases y;//;#n;nnormalize;ncases n;//;
558 ##|##*:#n;ncases y;//]
559 nqed.
560
561 ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
562 #x;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
563 ##[nrewrite > (Zsucc_Zpred ?);//
564 ##|#Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//]
565 nqed.
566
567 ntheorem associative_Zplus: associative Z Zplus.
568 (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
569 #x;#y;#z;ncases x
570 ##[//
571 ##|#n;nelim n
572    ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;
573    ##|#n1;#IH;
574       nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);
575       nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]
576 ##|#n;nelim n
577    ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;
578    ##|#n1;#IH;
579       nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);
580       nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]
581 ##]
582 nqed.
583
584 (* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
585 \def associative_Zplus. *)
586
587 (* Zopp *)
588 ndefinition Zopp : Z → Z ≝
589   λx:Z. match x with
590   [ OZ ⇒ OZ
591   | pos n ⇒ neg n
592   | neg n ⇒ pos n ].
593
594 interpretation "integer unary minus" 'uminus x = (Zopp x).
595
596 ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ).
597 //;
598 nqed.
599
600 ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
601 #x;#y;ncases x
602 ##[ncases y;//
603 ##|##*:#n;ncases y;//;#m;nnormalize;napply nat_compare_elim;nnormalize;//]
604 nqed.
605
606 ntheorem Zopp_Zopp: ∀x:Z. --x = x.
607 #x;ncases x;//;
608 nqed.
609
610 ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
611 #x;ncases x
612 ##[//
613 ##|##*:#n;nnormalize;nrewrite > (nat_compare_n_n ?);//]
614 nqed.
615
616 ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
617 #x;#z;#y;#H;
618 nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y);
619 nrewrite < (Zplus_Zopp x);
620 nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???);
621 //;
622 nqed.
623
624 ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
625 #x;#z;#y;#H;
626 napply (injective_Zplus_l x);
627 nrewrite < (sym_Zplus ??);
628 //;
629 nqed.
630
631 (* minus *)
632 ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
633
634 interpretation "integer minus" 'minus x y = (Zminus x y).