matitaB/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).