helm/software/matita/contribs/procedural/Coq/Reals/RIneq.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#**********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
  22
  23 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
  24
  25 (*   \VV/  *************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the      *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1       *)
  30
  31 (*#**********************************************************************)
  32
  33 (*i $Id: RIneq.v,v 1.23 2003/12/15 19:48:20 barras Exp $ i*)
  34
  35 (*#**************************************************************************)
  36
  37 (*#*              Basic lemmas for the classical reals numbers              *)
  38
  39 (*#**************************************************************************)
  40
  41 include "Reals/Raxioms.ma".
  42
  43 (* UNEXPORTED
  44 Open Local Scope Z_scope.
  45 *)
  46
  47 (* UNEXPORTED
  48 Open Local Scope R_scope.
  49 *)
  50
  51 (* UNEXPORTED
  52 Implicit Type r : R.
  53 *)
  54
  55 (*#**************************************************************************)
  56
  57 (*#*       Instantiating Ring tactic on reals                               *)
  58
  59 (*#**************************************************************************)
  60
  61 inline procedural "cic:/Coq/Reals/RIneq/RTheory.con" as lemma.
  62
  63 (* NOTATION
  64 Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
  65  with minus := Rminus div := Rdiv.
  66 *)
  67
  68 (*#*************************************************************************)
  69
  70 (*#*  Relation between orders and equality                                 *)
  71
  72 (*#*************************************************************************)
  73
  74 (*#*********)
  75
  76 inline procedural "cic:/Coq/Reals/RIneq/Rlt_irrefl.con" as lemma.
  77
  78 (* UNEXPORTED
  79 Hint Resolve Rlt_irrefl: real.
  80 *)
  81
  82 inline procedural "cic:/Coq/Reals/RIneq/Rle_refl.con" as lemma.
  83
  84 inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_eq.con" as lemma.
  85
  86 inline procedural "cic:/Coq/Reals/RIneq/Rgt_not_eq.con" as lemma.
  87
  88 (*#*********)
  89
  90 inline procedural "cic:/Coq/Reals/RIneq/Rlt_dichotomy_converse.con" as lemma.
  91
  92 (* UNEXPORTED
  93 Hint Resolve Rlt_dichotomy_converse: real.
  94 *)
  95
  96 (*#* Reasoning by case on equalities and order *)
  97
  98 (*#*********)
  99
 100 inline procedural "cic:/Coq/Reals/RIneq/Req_dec.con" as lemma.
 101
 102 (* UNEXPORTED
 103 Hint Resolve Req_dec: real.
 104 *)
 105
 106 (*#*********)
 107
 108 inline procedural "cic:/Coq/Reals/RIneq/Rtotal_order.con" as lemma.
 109
 110 (*#*********)
 111
 112 inline procedural "cic:/Coq/Reals/RIneq/Rdichotomy.con" as lemma.
 113
 114 (*#********************************************************************************)
 115
 116 (*#*       Order Lemma  : relating [<], [>], [<=] and [>=]                       *)
 117
 118 (*#********************************************************************************)
 119
 120 (*#*********)
 121
 122 inline procedural "cic:/Coq/Reals/RIneq/Rlt_le.con" as lemma.
 123
 124 (* UNEXPORTED
 125 Hint Resolve Rlt_le: real.
 126 *)
 127
 128 (*#*********)
 129
 130 inline procedural "cic:/Coq/Reals/RIneq/Rle_ge.con" as lemma.
 131
 132 (* UNEXPORTED
 133 Hint Immediate Rle_ge: real.
 134 *)
 135
 136 (*#*********)
 137
 138 inline procedural "cic:/Coq/Reals/RIneq/Rge_le.con" as lemma.
 139
 140 (* UNEXPORTED
 141 Hint Resolve Rge_le: real.
 142 *)
 143
 144 (*#*********)
 145
 146 inline procedural "cic:/Coq/Reals/RIneq/Rnot_le_lt.con" as lemma.
 147
 148 (* UNEXPORTED
 149 Hint Immediate Rnot_le_lt: real.
 150 *)
 151
 152 inline procedural "cic:/Coq/Reals/RIneq/Rnot_ge_lt.con" as lemma.
 153
 154 (*#*********)
 155
 156 inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_le.con" as lemma.
 157
 158 inline procedural "cic:/Coq/Reals/RIneq/Rgt_not_le.con" as lemma.
 159
 160 (* UNEXPORTED
 161 Hint Immediate Rlt_not_le: real.
 162 *)
 163
 164 inline procedural "cic:/Coq/Reals/RIneq/Rle_not_lt.con" as lemma.
 165
 166 (*#*********)
 167
 168 inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_ge.con" as lemma.
 169
 170 (* UNEXPORTED
 171 Hint Immediate Rlt_not_ge: real.
 172 *)
 173
 174 (*#*********)
 175
 176 inline procedural "cic:/Coq/Reals/RIneq/Req_le.con" as lemma.
 177
 178 (* UNEXPORTED
 179 Hint Immediate Req_le: real.
 180 *)
 181
 182 inline procedural "cic:/Coq/Reals/RIneq/Req_ge.con" as lemma.
 183
 184 (* UNEXPORTED
 185 Hint Immediate Req_ge: real.
 186 *)
 187
 188 inline procedural "cic:/Coq/Reals/RIneq/Req_le_sym.con" as lemma.
 189
 190 (* UNEXPORTED
 191 Hint Immediate Req_le_sym: real.
 192 *)
 193
 194 inline procedural "cic:/Coq/Reals/RIneq/Req_ge_sym.con" as lemma.
 195
 196 (* UNEXPORTED
 197 Hint Immediate Req_ge_sym: real.
 198 *)
 199
 200 inline procedural "cic:/Coq/Reals/RIneq/Rle_antisym.con" as lemma.
 201
 202 (* UNEXPORTED
 203 Hint Resolve Rle_antisym: real.
 204 *)
 205
 206 (*#*********)
 207
 208 inline procedural "cic:/Coq/Reals/RIneq/Rle_le_eq.con" as lemma.
 209
 210 inline procedural "cic:/Coq/Reals/RIneq/Rlt_eq_compat.con" as lemma.
 211
 212 (*#*********)
 213
 214 inline procedural "cic:/Coq/Reals/RIneq/Rle_trans.con" as lemma.
 215
 216 (*#*********)
 217
 218 inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_trans.con" as lemma.
 219
 220 (*#*********)
 221
 222 inline procedural "cic:/Coq/Reals/RIneq/Rlt_le_trans.con" as lemma.
 223
 224 (*#* Decidability of the order *)
 225
 226 inline procedural "cic:/Coq/Reals/RIneq/Rlt_dec.con" as lemma.
 227
 228 (*#*********)
 229
 230 inline procedural "cic:/Coq/Reals/RIneq/Rle_dec.con" as lemma.
 231
 232 (*#*********)
 233
 234 inline procedural "cic:/Coq/Reals/RIneq/Rgt_dec.con" as lemma.
 235
 236 (*#*********)
 237
 238 inline procedural "cic:/Coq/Reals/RIneq/Rge_dec.con" as lemma.
 239
 240 inline procedural "cic:/Coq/Reals/RIneq/Rlt_le_dec.con" as lemma.
 241
 242 inline procedural "cic:/Coq/Reals/RIneq/Rle_or_lt.con" as lemma.
 243
 244 inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_or_eq_dec.con" as lemma.
 245
 246 (*#*********)
 247
 248 inline procedural "cic:/Coq/Reals/RIneq/inser_trans_R.con" as lemma.
 249
 250 (*#***************************************************************)
 251
 252 (*#*        Field Lemmas                                         *)
 253
 254 (* This part contains lemma involving the Fields operations     *)
 255
 256 (*#***************************************************************)
 257
 258 (*#********************************************************)
 259
 260 (*#*      Addition                                        *)
 261
 262 (*#********************************************************)
 263
 264 inline procedural "cic:/Coq/Reals/RIneq/Rplus_ne.con" as lemma.
 265
 266 (* UNEXPORTED
 267 Hint Resolve Rplus_ne: real v62.
 268 *)
 269
 270 inline procedural "cic:/Coq/Reals/RIneq/Rplus_0_r.con" as lemma.
 271
 272 (* UNEXPORTED
 273 Hint Resolve Rplus_0_r: real.
 274 *)
 275
 276 (*#*********)
 277
 278 inline procedural "cic:/Coq/Reals/RIneq/Rplus_opp_l.con" as lemma.
 279
 280 (* UNEXPORTED
 281 Hint Resolve Rplus_opp_l: real.
 282 *)
 283
 284 (*#*********)
 285
 286 inline procedural "cic:/Coq/Reals/RIneq/Rplus_opp_r_uniq.con" as lemma.
 287
 288 (*i New i*)
 289
 290 (* UNEXPORTED
 291 Hint Resolve (f_equal (A:=R)): real.
 292 *)
 293
 294 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_compat_l.con" as lemma.
 295
 296 (*i Old i*)
 297
 298 (* UNEXPORTED
 299 Hint Resolve Rplus_eq_compat_l: v62.
 300 *)
 301
 302 (*#*********)
 303
 304 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_reg_l.con" as lemma.
 305
 306 (* UNEXPORTED
 307 Hint Resolve Rplus_eq_reg_l: real.
 308 *)
 309
 310 (*#*********)
 311
 312 inline procedural "cic:/Coq/Reals/RIneq/Rplus_0_r_uniq.con" as lemma.
 313
 314 (*#**********************************************************)
 315
 316 (*#*       Multiplication                                   *)
 317
 318 (*#**********************************************************)
 319
 320 (*#*********)
 321
 322 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r.con" as lemma.
 323
 324 (* UNEXPORTED
 325 Hint Resolve Rinv_r: real.
 326 *)
 327
 328 inline procedural "cic:/Coq/Reals/RIneq/Rinv_l_sym.con" as lemma.
 329
 330 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_sym.con" as lemma.
 331
 332 (* UNEXPORTED
 333 Hint Resolve Rinv_l_sym Rinv_r_sym: real.
 334 *)
 335
 336 (*#*********)
 337
 338 inline procedural "cic:/Coq/Reals/RIneq/Rmult_0_r.con" as lemma.
 339
 340 (* UNEXPORTED
 341 Hint Resolve Rmult_0_r: real v62.
 342 *)
 343
 344 (*#*********)
 345
 346 inline procedural "cic:/Coq/Reals/RIneq/Rmult_0_l.con" as lemma.
 347
 348 (* UNEXPORTED
 349 Hint Resolve Rmult_0_l: real v62.
 350 *)
 351
 352 (*#*********)
 353
 354 inline procedural "cic:/Coq/Reals/RIneq/Rmult_ne.con" as lemma.
 355
 356 (* UNEXPORTED
 357 Hint Resolve Rmult_ne: real v62.
 358 *)
 359
 360 (*#*********)
 361
 362 inline procedural "cic:/Coq/Reals/RIneq/Rmult_1_r.con" as lemma.
 363
 364 (* UNEXPORTED
 365 Hint Resolve Rmult_1_r: real.
 366 *)
 367
 368 (*#*********)
 369
 370 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_compat_l.con" as lemma.
 371
 372 (*i OLD i*)
 373
 374 (* UNEXPORTED
 375 Hint Resolve Rmult_eq_compat_l: v62.
 376 *)
 377
 378 (*#*********)
 379
 380 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_reg_l.con" as lemma.
 381
 382 (*#*********)
 383
 384 inline procedural "cic:/Coq/Reals/RIneq/Rmult_integral.con" as lemma.
 385
 386 (*#*********)
 387
 388 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat.con" as lemma.
 389
 390 (* UNEXPORTED
 391 Hint Resolve Rmult_eq_0_compat: real.
 392 *)
 393
 394 (*#*********)
 395
 396 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_r.con" as lemma.
 397
 398 (*#*********)
 399
 400 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_l.con" as lemma.
 401
 402 (*#*********)
 403
 404 inline procedural "cic:/Coq/Reals/RIneq/Rmult_neq_0_reg.con" as lemma.
 405
 406 (*#*********)
 407
 408 inline procedural "cic:/Coq/Reals/RIneq/Rmult_integral_contrapositive.con" as lemma.
 409
 410 (* UNEXPORTED
 411 Hint Resolve Rmult_integral_contrapositive: real.
 412 *)
 413
 414 (*#*********)
 415
 416 inline procedural "cic:/Coq/Reals/RIneq/Rmult_plus_distr_r.con" as lemma.
 417
 418 (*#* Square function *)
 419
 420 (*#**********)
 421
 422 inline procedural "cic:/Coq/Reals/RIneq/Rsqr.con" as definition.
 423
 424 (*#**********)
 425
 426 inline procedural "cic:/Coq/Reals/RIneq/Rsqr_0.con" as lemma.
 427
 428 (*#**********)
 429
 430 inline procedural "cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con" as lemma.
 431
 432 (*#********************************************************)
 433
 434 (*#*      Opposite                                        *)
 435
 436 (*#********************************************************)
 437
 438 (*#*********)
 439
 440 inline procedural "cic:/Coq/Reals/RIneq/Ropp_eq_compat.con" as lemma.
 441
 442 (* UNEXPORTED
 443 Hint Resolve Ropp_eq_compat: real.
 444 *)
 445
 446 (*#*********)
 447
 448 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0.con" as lemma.
 449
 450 (* UNEXPORTED
 451 Hint Resolve Ropp_0: real v62.
 452 *)
 453
 454 (*#*********)
 455
 456 inline procedural "cic:/Coq/Reals/RIneq/Ropp_eq_0_compat.con" as lemma.
 457
 458 (* UNEXPORTED
 459 Hint Resolve Ropp_eq_0_compat: real.
 460 *)
 461
 462 (*#*********)
 463
 464 inline procedural "cic:/Coq/Reals/RIneq/Ropp_involutive.con" as lemma.
 465
 466 (* UNEXPORTED
 467 Hint Resolve Ropp_involutive: real.
 468 *)
 469
 470 (*#********)
 471
 472 inline procedural "cic:/Coq/Reals/RIneq/Ropp_neq_0_compat.con" as lemma.
 473
 474 (* UNEXPORTED
 475 Hint Resolve Ropp_neq_0_compat: real.
 476 *)
 477
 478 (*#*********)
 479
 480 inline procedural "cic:/Coq/Reals/RIneq/Ropp_plus_distr.con" as lemma.
 481
 482 (* UNEXPORTED
 483 Hint Resolve Ropp_plus_distr: real.
 484 *)
 485
 486 (*#* Opposite and multiplication *)
 487
 488 inline procedural "cic:/Coq/Reals/RIneq/Ropp_mult_distr_l_reverse.con" as lemma.
 489
 490 (* UNEXPORTED
 491 Hint Resolve Ropp_mult_distr_l_reverse: real.
 492 *)
 493
 494 (*#*********)
 495
 496 inline procedural "cic:/Coq/Reals/RIneq/Rmult_opp_opp.con" as lemma.
 497
 498 (* UNEXPORTED
 499 Hint Resolve Rmult_opp_opp: real.
 500 *)
 501
 502 inline procedural "cic:/Coq/Reals/RIneq/Ropp_mult_distr_r_reverse.con" as lemma.
 503
 504 (*#* Substraction *)
 505
 506 inline procedural "cic:/Coq/Reals/RIneq/Rminus_0_r.con" as lemma.
 507
 508 (* UNEXPORTED
 509 Hint Resolve Rminus_0_r: real.
 510 *)
 511
 512 inline procedural "cic:/Coq/Reals/RIneq/Rminus_0_l.con" as lemma.
 513
 514 (* UNEXPORTED
 515 Hint Resolve Rminus_0_l: real.
 516 *)
 517
 518 (*#*********)
 519
 520 inline procedural "cic:/Coq/Reals/RIneq/Ropp_minus_distr.con" as lemma.
 521
 522 (* UNEXPORTED
 523 Hint Resolve Ropp_minus_distr: real.
 524 *)
 525
 526 inline procedural "cic:/Coq/Reals/RIneq/Ropp_minus_distr'.con" as lemma.
 527
 528 (* UNEXPORTED
 529 Hint Resolve Ropp_minus_distr': real.
 530 *)
 531
 532 (*#*********)
 533
 534 inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_eq.con" as lemma.
 535
 536 (* UNEXPORTED
 537 Hint Resolve Rminus_diag_eq: real.
 538 *)
 539
 540 (*#*********)
 541
 542 inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_uniq.con" as lemma.
 543
 544 (* UNEXPORTED
 545 Hint Immediate Rminus_diag_uniq: real.
 546 *)
 547
 548 inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_uniq_sym.con" as lemma.
 549
 550 (* UNEXPORTED
 551 Hint Immediate Rminus_diag_uniq_sym: real.
 552 *)
 553
 554 inline procedural "cic:/Coq/Reals/RIneq/Rplus_minus.con" as lemma.
 555
 556 (* UNEXPORTED
 557 Hint Resolve Rplus_minus: real.
 558 *)
 559
 560 (*#*********)
 561
 562 inline procedural "cic:/Coq/Reals/RIneq/Rminus_eq_contra.con" as lemma.
 563
 564 (* UNEXPORTED
 565 Hint Resolve Rminus_eq_contra: real.
 566 *)
 567
 568 inline procedural "cic:/Coq/Reals/RIneq/Rminus_not_eq.con" as lemma.
 569
 570 (* UNEXPORTED
 571 Hint Resolve Rminus_not_eq: real.
 572 *)
 573
 574 inline procedural "cic:/Coq/Reals/RIneq/Rminus_not_eq_right.con" as lemma.
 575
 576 (* UNEXPORTED
 577 Hint Resolve Rminus_not_eq_right: real.
 578 *)
 579
 580 (*#*********)
 581
 582 inline procedural "cic:/Coq/Reals/RIneq/Rmult_minus_distr_l.con" as lemma.
 583
 584 (*#* Inverse *)
 585
 586 inline procedural "cic:/Coq/Reals/RIneq/Rinv_1.con" as lemma.
 587
 588 (* UNEXPORTED
 589 Hint Resolve Rinv_1: real.
 590 *)
 591
 592 (*#********)
 593
 594 inline procedural "cic:/Coq/Reals/RIneq/Rinv_neq_0_compat.con" as lemma.
 595
 596 (* UNEXPORTED
 597 Hint Resolve Rinv_neq_0_compat: real.
 598 *)
 599
 600 (*#********)
 601
 602 inline procedural "cic:/Coq/Reals/RIneq/Rinv_involutive.con" as lemma.
 603
 604 (* UNEXPORTED
 605 Hint Resolve Rinv_involutive: real.
 606 *)
 607
 608 (*#********)
 609
 610 inline procedural "cic:/Coq/Reals/RIneq/Rinv_mult_distr.con" as lemma.
 611
 612 (*#********)
 613
 614 inline procedural "cic:/Coq/Reals/RIneq/Ropp_inv_permute.con" as lemma.
 615
 616 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_r.con" as lemma.
 617
 618 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_l.con" as lemma.
 619
 620 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_m.con" as lemma.
 621
 622 (* UNEXPORTED
 623 Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real.
 624 *)
 625
 626 (*#********)
 627
 628 inline procedural "cic:/Coq/Reals/RIneq/Rinv_mult_simpl.con" as lemma.
 629
 630 (*#* Order and addition *)
 631
 632 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_compat_r.con" as lemma.
 633
 634 (* UNEXPORTED
 635 Hint Resolve Rplus_lt_compat_r: real.
 636 *)
 637
 638 (*#*********)
 639
 640 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_reg_r.con" as lemma.
 641
 642 (*#*********)
 643
 644 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat_l.con" as lemma.
 645
 646 (*#*********)
 647
 648 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat_r.con" as lemma.
 649
 650 (* UNEXPORTED
 651 Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.
 652 *)
 653
 654 (*#*********)
 655
 656 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_reg_l.con" as lemma.
 657
 658 (*#*********)
 659
 660 inline procedural "cic:/Coq/Reals/RIneq/sum_inequa_Rle_lt.con" as lemma.
 661
 662 (*#********)
 663
 664 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_compat.con" as lemma.
 665
 666 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat.con" as lemma.
 667
 668 (*#********)
 669
 670 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_le_compat.con" as lemma.
 671
 672 (*#********)
 673
 674 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_lt_compat.con" as lemma.
 675
 676 (* UNEXPORTED
 677 Hint Immediate Rplus_lt_compat Rplus_le_compat Rplus_lt_le_compat
 678   Rplus_le_lt_compat: real.
 679 *)
 680
 681 (*#* Order and Opposite *)
 682
 683 (*#*********)
 684
 685 inline procedural "cic:/Coq/Reals/RIneq/Ropp_gt_lt_contravar.con" as lemma.
 686
 687 (* UNEXPORTED
 688 Hint Resolve Ropp_gt_lt_contravar.
 689 *)
 690
 691 (*#*********)
 692
 693 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_gt_contravar.con" as lemma.
 694
 695 (* UNEXPORTED
 696 Hint Resolve Ropp_lt_gt_contravar: real.
 697 *)
 698
 699 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_cancel.con" as lemma.
 700
 701 (* UNEXPORTED
 702 Hint Immediate Ropp_lt_cancel: real.
 703 *)
 704
 705 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_contravar.con" as lemma.
 706
 707 (* UNEXPORTED
 708 Hint Resolve Ropp_lt_contravar: real.
 709 *)
 710
 711 (*#*********)
 712
 713 inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_ge_contravar.con" as lemma.
 714
 715 (* UNEXPORTED
 716 Hint Resolve Ropp_le_ge_contravar: real.
 717 *)
 718
 719 inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_cancel.con" as lemma.
 720
 721 (* UNEXPORTED
 722 Hint Immediate Ropp_le_cancel: real.
 723 *)
 724
 725 inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_contravar.con" as lemma.
 726
 727 (* UNEXPORTED
 728 Hint Resolve Ropp_le_contravar: real.
 729 *)
 730
 731 (*#*********)
 732
 733 inline procedural "cic:/Coq/Reals/RIneq/Ropp_ge_le_contravar.con" as lemma.
 734
 735 (* UNEXPORTED
 736 Hint Resolve Ropp_ge_le_contravar: real.
 737 *)
 738
 739 (*#*********)
 740
 741 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_lt_gt_contravar.con" as lemma.
 742
 743 (* UNEXPORTED
 744 Hint Resolve Ropp_0_lt_gt_contravar: real.
 745 *)
 746
 747 (*#*********)
 748
 749 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_gt_lt_contravar.con" as lemma.
 750
 751 (* UNEXPORTED
 752 Hint Resolve Ropp_0_gt_lt_contravar: real.
 753 *)
 754
 755 (*#*********)
 756
 757 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_gt_0_contravar.con" as lemma.
 758
 759 (*#*********)
 760
 761 inline procedural "cic:/Coq/Reals/RIneq/Ropp_gt_lt_0_contravar.con" as lemma.
 762
 763 (* UNEXPORTED
 764 Hint Resolve Ropp_lt_gt_0_contravar Ropp_gt_lt_0_contravar: real.
 765 *)
 766
 767 (*#*********)
 768
 769 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_le_ge_contravar.con" as lemma.
 770
 771 (* UNEXPORTED
 772 Hint Resolve Ropp_0_le_ge_contravar: real.
 773 *)
 774
 775 (*#*********)
 776
 777 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_ge_le_contravar.con" as lemma.
 778
 779 (* UNEXPORTED
 780 Hint Resolve Ropp_0_ge_le_contravar: real.
 781 *)
 782
 783 (*#* Order and multiplication *)
 784
 785 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_compat_r.con" as lemma.
 786
 787 (* UNEXPORTED
 788 Hint Resolve Rmult_lt_compat_r.
 789 *)
 790
 791 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_reg_l.con" as lemma.
 792
 793 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_gt_compat_neg_l.con" as lemma.
 794
 795 (*#*********)
 796
 797 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_l.con" as lemma.
 798
 799 (* UNEXPORTED
 800 Hint Resolve Rmult_le_compat_l: real.
 801 *)
 802
 803 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_r.con" as lemma.
 804
 805 (* UNEXPORTED
 806 Hint Resolve Rmult_le_compat_r: real.
 807 *)
 808
 809 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_reg_l.con" as lemma.
 810
 811 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_neg_l.con" as lemma.
 812
 813 (* UNEXPORTED
 814 Hint Resolve Rmult_le_compat_neg_l: real.
 815 *)
 816
 817 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_ge_compat_neg_l.con" as lemma.
 818
 819 (* UNEXPORTED
 820 Hint Resolve Rmult_le_ge_compat_neg_l: real.
 821 *)
 822
 823 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat.con" as lemma.
 824
 825 (* UNEXPORTED
 826 Hint Resolve Rmult_le_compat: real.
 827 *)
 828
 829 inline procedural "cic:/Coq/Reals/RIneq/Rmult_gt_0_lt_compat.con" as lemma.
 830
 831 (*#********)
 832
 833 inline procedural "cic:/Coq/Reals/RIneq/Rmult_ge_0_gt_0_lt_compat.con" as lemma.
 834
 835 (*#* Order and Substractions *)
 836
 837 inline procedural "cic:/Coq/Reals/RIneq/Rlt_minus.con" as lemma.
 838
 839 (* UNEXPORTED
 840 Hint Resolve Rlt_minus: real.
 841 *)
 842
 843 (*#*********)
 844
 845 inline procedural "cic:/Coq/Reals/RIneq/Rle_minus.con" as lemma.
 846
 847 (*#*********)
 848
 849 inline procedural "cic:/Coq/Reals/RIneq/Rminus_lt.con" as lemma.
 850
 851 (*#*********)
 852
 853 inline procedural "cic:/Coq/Reals/RIneq/Rminus_le.con" as lemma.
 854
 855 (*#*********)
 856
 857 inline procedural "cic:/Coq/Reals/RIneq/tech_Rplus.con" as lemma.
 858
 859 (* UNEXPORTED
 860 Hint Immediate tech_Rplus: real.
 861 *)
 862
 863 (*#* Order and the square function *)
 864
 865 inline procedural "cic:/Coq/Reals/RIneq/Rle_0_sqr.con" as lemma.
 866
 867 (*#**********)
 868
 869 inline procedural "cic:/Coq/Reals/RIneq/Rlt_0_sqr.con" as lemma.
 870
 871 (* UNEXPORTED
 872 Hint Resolve Rle_0_sqr Rlt_0_sqr: real.
 873 *)
 874
 875 (*#* Zero is less than one *)
 876
 877 inline procedural "cic:/Coq/Reals/RIneq/Rlt_0_1.con" as lemma.
 878
 879 (* UNEXPORTED
 880 Hint Resolve Rlt_0_1: real.
 881 *)
 882
 883 inline procedural "cic:/Coq/Reals/RIneq/Rle_0_1.con" as lemma.
 884
 885 (*#* Order and inverse *)
 886
 887 inline procedural "cic:/Coq/Reals/RIneq/Rinv_0_lt_compat.con" as lemma.
 888
 889 (* UNEXPORTED
 890 Hint Resolve Rinv_0_lt_compat: real.
 891 *)
 892
 893 (*#********)
 894
 895 inline procedural "cic:/Coq/Reals/RIneq/Rinv_lt_0_compat.con" as lemma.
 896
 897 (* UNEXPORTED
 898 Hint Resolve Rinv_lt_0_compat: real.
 899 *)
 900
 901 (*#********)
 902
 903 inline procedural "cic:/Coq/Reals/RIneq/Rinv_lt_contravar.con" as lemma.
 904
 905 inline procedural "cic:/Coq/Reals/RIneq/Rinv_1_lt_contravar.con" as lemma.
 906
 907 (* UNEXPORTED
 908 Hint Resolve Rinv_1_lt_contravar: real.
 909 *)
 910
 911 (*#********************************************************)
 912
 913 (*#*      Greater                                         *)
 914
 915 (*#********************************************************)
 916
 917 (*#*********)
 918
 919 inline procedural "cic:/Coq/Reals/RIneq/Rge_antisym.con" as lemma.
 920
 921 (*#*********)
 922
 923 inline procedural "cic:/Coq/Reals/RIneq/Rnot_lt_ge.con" as lemma.
 924
 925 (*#*********)
 926
 927 inline procedural "cic:/Coq/Reals/RIneq/Rnot_lt_le.con" as lemma.
 928
 929 (*#*********)
 930
 931 inline procedural "cic:/Coq/Reals/RIneq/Rnot_gt_le.con" as lemma.
 932
 933 (*#*********)
 934
 935 inline procedural "cic:/Coq/Reals/RIneq/Rgt_ge.con" as lemma.
 936
 937 (*#*********)
 938
 939 inline procedural "cic:/Coq/Reals/RIneq/Rge_gt_trans.con" as lemma.
 940
 941 (*#*********)
 942
 943 inline procedural "cic:/Coq/Reals/RIneq/Rgt_ge_trans.con" as lemma.
 944
 945 (*#*********)
 946
 947 inline procedural "cic:/Coq/Reals/RIneq/Rgt_trans.con" as lemma.
 948
 949 (*#*********)
 950
 951 inline procedural "cic:/Coq/Reals/RIneq/Rge_trans.con" as lemma.
 952
 953 (*#*********)
 954
 955 inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_0_plus_1.con" as lemma.
 956
 957 (* UNEXPORTED
 958 Hint Resolve Rle_lt_0_plus_1: real.
 959 *)
 960
 961 (*#*********)
 962
 963 inline procedural "cic:/Coq/Reals/RIneq/Rlt_plus_1.con" as lemma.
 964
 965 (* UNEXPORTED
 966 Hint Resolve Rlt_plus_1: real.
 967 *)
 968
 969 (*#*********)
 970
 971 inline procedural "cic:/Coq/Reals/RIneq/tech_Rgt_minus.con" as lemma.
 972
 973 (*#**********)
 974
 975 inline procedural "cic:/Coq/Reals/RIneq/Rplus_gt_compat_l.con" as lemma.
 976
 977 (* UNEXPORTED
 978 Hint Resolve Rplus_gt_compat_l: real.
 979 *)
 980
 981 (*#**********)
 982
 983 inline procedural "cic:/Coq/Reals/RIneq/Rplus_gt_reg_l.con" as lemma.
 984
 985 (*#**********)
 986
 987 inline procedural "cic:/Coq/Reals/RIneq/Rplus_ge_compat_l.con" as lemma.
 988
 989 (* UNEXPORTED
 990 Hint Resolve Rplus_ge_compat_l: real.
 991 *)
 992
 993 (*#**********)
 994
 995 inline procedural "cic:/Coq/Reals/RIneq/Rplus_ge_reg_l.con" as lemma.
 996
 997 (*#**********)
 998
 999 inline procedural "cic:/Coq/Reals/RIneq/Rmult_ge_compat_r.con" as lemma.
1000
1001 (*#**********)
1002
1003 inline procedural "cic:/Coq/Reals/RIneq/Rgt_minus.con" as lemma.
1004
1005 (*#********)
1006
1007 inline procedural "cic:/Coq/Reals/RIneq/minus_Rgt.con" as lemma.
1008
1009 (*#*********)
1010
1011 inline procedural "cic:/Coq/Reals/RIneq/Rge_minus.con" as lemma.
1012
1013 (*#********)
1014
1015 inline procedural "cic:/Coq/Reals/RIneq/minus_Rge.con" as lemma.
1016
1017 (*#********)
1018
1019 inline procedural "cic:/Coq/Reals/RIneq/Rmult_gt_0_compat.con" as lemma.
1020
1021 (*#********)
1022
1023 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_0_compat.con" as lemma.
1024
1025 (*#**********)
1026
1027 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_0_l.con" as lemma.
1028
1029 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_R0.con" as lemma.
1030
1031 (*#**********)
1032
1033 inline procedural "cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0_l.con" as lemma.
1034
1035 inline procedural "cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0.con" as lemma.
1036
1037 (*#*********************************************************)
1038
1039 (*#*       Injection from [N] to [R]                       *)
1040
1041 (*#*********************************************************)
1042
1043 (*#*********)
1044
1045 inline procedural "cic:/Coq/Reals/RIneq/S_INR.con" as lemma.
1046
1047 (*#*********)
1048
1049 inline procedural "cic:/Coq/Reals/RIneq/S_O_plus_INR.con" as lemma.
1050
1051 (*#*********)
1052
1053 inline procedural "cic:/Coq/Reals/RIneq/plus_INR.con" as lemma.
1054
1055 (*#*********)
1056
1057 inline procedural "cic:/Coq/Reals/RIneq/minus_INR.con" as lemma.
1058
1059 (*#********)
1060
1061 inline procedural "cic:/Coq/Reals/RIneq/mult_INR.con" as lemma.
1062
1063 (* UNEXPORTED
1064 Hint Resolve plus_INR minus_INR mult_INR: real.
1065 *)
1066
1067 (*#********)
1068
1069 inline procedural "cic:/Coq/Reals/RIneq/lt_INR_0.con" as lemma.
1070
1071 (* UNEXPORTED
1072 Hint Resolve lt_INR_0: real.
1073 *)
1074
1075 inline procedural "cic:/Coq/Reals/RIneq/lt_INR.con" as lemma.
1076
1077 (* UNEXPORTED
1078 Hint Resolve lt_INR: real.
1079 *)
1080
1081 inline procedural "cic:/Coq/Reals/RIneq/INR_lt_1.con" as lemma.
1082
1083 (* UNEXPORTED
1084 Hint Resolve INR_lt_1: real.
1085 *)
1086
1087 (*#*********)
1088
1089 inline procedural "cic:/Coq/Reals/RIneq/INR_pos.con" as lemma.
1090
1091 (* UNEXPORTED
1092 Hint Resolve INR_pos: real.
1093 *)
1094
1095 (*#*********)
1096
1097 inline procedural "cic:/Coq/Reals/RIneq/pos_INR.con" as lemma.
1098
1099 (* UNEXPORTED
1100 Hint Resolve pos_INR: real.
1101 *)
1102
1103 inline procedural "cic:/Coq/Reals/RIneq/INR_lt.con" as lemma.
1104
1105 (* UNEXPORTED
1106 Hint Resolve INR_lt: real.
1107 *)
1108
1109 (*#********)
1110
1111 inline procedural "cic:/Coq/Reals/RIneq/le_INR.con" as lemma.
1112
1113 (* UNEXPORTED
1114 Hint Resolve le_INR: real.
1115 *)
1116
1117 (*#*********)
1118
1119 inline procedural "cic:/Coq/Reals/RIneq/not_INR_O.con" as lemma.
1120
1121 (* UNEXPORTED
1122 Hint Immediate not_INR_O: real.
1123 *)
1124
1125 (*#*********)
1126
1127 inline procedural "cic:/Coq/Reals/RIneq/not_O_INR.con" as lemma.
1128
1129 (* UNEXPORTED
1130 Hint Resolve not_O_INR: real.
1131 *)
1132
1133 inline procedural "cic:/Coq/Reals/RIneq/not_nm_INR.con" as lemma.
1134
1135 (* UNEXPORTED
1136 Hint Resolve not_nm_INR: real.
1137 *)
1138
1139 inline procedural "cic:/Coq/Reals/RIneq/INR_eq.con" as lemma.
1140
1141 (* UNEXPORTED
1142 Hint Resolve INR_eq: real.
1143 *)
1144
1145 inline procedural "cic:/Coq/Reals/RIneq/INR_le.con" as lemma.
1146
1147 (* UNEXPORTED
1148 Hint Resolve INR_le: real.
1149 *)
1150
1151 inline procedural "cic:/Coq/Reals/RIneq/not_1_INR.con" as lemma.
1152
1153 (* UNEXPORTED
1154 Hint Resolve not_1_INR: real.
1155 *)
1156
1157 (*#*********************************************************)
1158
1159 (*#*      Injection from [Z] to [R]                        *)
1160
1161 (*#*********************************************************)
1162
1163 (*#*********)
1164
1165 inline procedural "cic:/Coq/Reals/RIneq/IZN.con" as lemma.
1166
1167 (*#*********)
1168
1169 inline procedural "cic:/Coq/Reals/RIneq/INR_IZR_INZ.con" as lemma.
1170
1171 inline procedural "cic:/Coq/Reals/RIneq/plus_IZR_NEG_POS.con" as lemma.
1172
1173 (*#*********)
1174
1175 inline procedural "cic:/Coq/Reals/RIneq/plus_IZR.con" as lemma.
1176
1177 (*#*********)
1178
1179 inline procedural "cic:/Coq/Reals/RIneq/mult_IZR.con" as lemma.
1180
1181 (*#*********)
1182
1183 inline procedural "cic:/Coq/Reals/RIneq/Ropp_Ropp_IZR.con" as lemma.
1184
1185 (*#*********)
1186
1187 inline procedural "cic:/Coq/Reals/RIneq/Z_R_minus.con" as lemma.
1188
1189 (*#*********)
1190
1191 inline procedural "cic:/Coq/Reals/RIneq/lt_O_IZR.con" as lemma.
1192
1193 (*#*********)
1194
1195 inline procedural "cic:/Coq/Reals/RIneq/lt_IZR.con" as lemma.
1196
1197 (*#*********)
1198
1199 inline procedural "cic:/Coq/Reals/RIneq/eq_IZR_R0.con" as lemma.
1200
1201 (*#*********)
1202
1203 inline procedural "cic:/Coq/Reals/RIneq/eq_IZR.con" as lemma.
1204
1205 (*#*********)
1206
1207 inline procedural "cic:/Coq/Reals/RIneq/not_O_IZR.con" as lemma.
1208
1209 (*#********)
1210
1211 inline procedural "cic:/Coq/Reals/RIneq/le_O_IZR.con" as lemma.
1212
1213 (*#*********)
1214
1215 inline procedural "cic:/Coq/Reals/RIneq/le_IZR.con" as lemma.
1216
1217 (*#*********)
1218
1219 inline procedural "cic:/Coq/Reals/RIneq/le_IZR_R1.con" as lemma.
1220
1221 (*#*********)
1222
1223 inline procedural "cic:/Coq/Reals/RIneq/IZR_ge.con" as lemma.
1224
1225 inline procedural "cic:/Coq/Reals/RIneq/IZR_le.con" as lemma.
1226
1227 inline procedural "cic:/Coq/Reals/RIneq/IZR_lt.con" as lemma.
1228
1229 inline procedural "cic:/Coq/Reals/RIneq/one_IZR_lt1.con" as lemma.
1230
1231 inline procedural "cic:/Coq/Reals/RIneq/one_IZR_r_R1.con" as lemma.
1232
1233 (*#*********)
1234
1235 inline procedural "cic:/Coq/Reals/RIneq/single_z_r_R1.con" as lemma.
1236
1237 (*#*********)
1238
1239 inline procedural "cic:/Coq/Reals/RIneq/tech_single_z_r_R1.con" as lemma.
1240
1241 (*#****************************************************************)
1242
1243 (*#* Definitions of new types                                     *)
1244
1245 (*#****************************************************************)
1246
1247 inline procedural "cic:/Coq/Reals/RIneq/nonnegreal.ind".
1248
1249 inline procedural "cic:/Coq/Reals/RIneq/posreal.ind".
1250
1251 inline procedural "cic:/Coq/Reals/RIneq/nonposreal.ind".
1252
1253 inline procedural "cic:/Coq/Reals/RIneq/negreal.ind".
1254
1255 inline procedural "cic:/Coq/Reals/RIneq/nonzeroreal.ind".
1256
1257 (*#*********)
1258
1259 inline procedural "cic:/Coq/Reals/RIneq/prod_neq_R0.con" as lemma.
1260
1261 (*#********)
1262
1263 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_pos.con" as lemma.
1264
1265 inline procedural "cic:/Coq/Reals/RIneq/double.con" as lemma.
1266
1267 inline procedural "cic:/Coq/Reals/RIneq/double_var.con" as lemma.
1268
1269 (*#*********************************************************)
1270
1271 (*#* Other rules about < and <=                            *)
1272
1273 (*#*********************************************************)
1274
1275 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con" as lemma.
1276
1277 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_lt_0_compat.con" as lemma.
1278
1279 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_le_0_compat.con" as lemma.
1280
1281 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_le_0_compat.con" as lemma.
1282
1283 inline procedural "cic:/Coq/Reals/RIneq/plus_le_is_le.con" as lemma.
1284
1285 inline procedural "cic:/Coq/Reals/RIneq/plus_lt_is_lt.con" as lemma.
1286
1287 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_0_lt_compat.con" as lemma.
1288
1289 inline procedural "cic:/Coq/Reals/RIneq/le_epsilon.con" as lemma.
1290
1291 (*#*********)
1292
1293 inline procedural "cic:/Coq/Reals/RIneq/completeness_weak.con" as lemma.
1294