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