helm/software/matita/contribs/procedural/CoRN/algebra/COrdFields.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 "CoRN.ma".
  18
  19 (* $Id: COrdFields.v,v 1.6 2004/04/23 10:00:52 lcf Exp $ *)
  20
  21 (*#* printing [<] %\ensuremath<% #&lt;# *)
  22
  23 (*#* printing [<=] %\ensuremath{\leq}% #&le;# *)
  24
  25 (*#* printing [>] %\ensuremath>% #&gt;# *)
  26
  27 (*#* printing OneNZ %\ensuremath{\mathbf1}% #1# *)
  28
  29 (*#* printing TwoNZ %\ensuremath{\mathbf2}% #2# *)
  30
  31 (*#* printing ThreeNZ %\ensuremath{\mathbf3}% #3# *)
  32
  33 (*#* printing FourNZ %\ensuremath{\mathbf4}% #4# *)
  34
  35 (*#* printing SixNZ %\ensuremath{\mathbf6}% #6# *)
  36
  37 (*#* printing EightNZ %\ensuremath{\mathbf8}% #8# *)
  38
  39 (*#* printing NineNZ %\ensuremath{\mathbf9}% #9# *)
  40
  41 (*#* printing TwelveNZ %\ensuremath{\mathbf{12}}% #12# *)
  42
  43 (*#* printing SixteenNZ %\ensuremath{\mathbf{16}}% #16# *)
  44
  45 (*#* printing EighteenNZ %\ensuremath{\mathbf{18}}% #18# *)
  46
  47 (*#* printing TwentyFourNZ %\ensuremath{\mathbf{24}}% #24# *)
  48
  49 (*#* printing FortyEightNZ %\ensuremath{\mathbf{48}}% #48# *)
  50
  51 include "tactics/FieldReflection.ma".
  52
  53 (* ORDERED FIELDS *)
  54
  55 (*#*
  56 * Ordered Fields
  57 ** Definition of the notion of ordered field
  58 *)
  59
  60 (* Begin_SpecReals *)
  61
  62 inline procedural "cic:/CoRN/algebra/COrdFields/strictorder.ind".
  63
  64 (* UNEXPORTED
  65 Implicit Arguments strictorder [A].
  66 *)
  67
  68 (* UNEXPORTED
  69 Implicit Arguments Build_strictorder [A R].
  70 *)
  71
  72 (* UNEXPORTED
  73 Implicit Arguments so_trans [A R].
  74 *)
  75
  76 (* UNEXPORTED
  77 Implicit Arguments so_asym [A R].
  78 *)
  79
  80 inline procedural "cic:/CoRN/algebra/COrdFields/is_COrdField.ind".
  81
  82 inline procedural "cic:/CoRN/algebra/COrdFields/COrdField.ind".
  83
  84 (* COERCION
  85 cic:/matita/CoRN-Procedural/algebra/COrdFields/cof_crr.con
  86 *)
  87
  88 (*#*
  89 %\begin{nameconvention}%
  90 In the names of lemmas, [ [<] ] is written as [less] and "[Zero [<] ]"
  91 is written as [pos].
  92 %\end{nameconvention}%
  93 *)
  94
  95 (* UNEXPORTED
  96 Implicit Arguments cof_less [c].
  97 *)
  98
  99 (* NOTATION
 100 Infix "[<]" := cof_less (at level 70, no associativity).
 101 *)
 102
 103 inline procedural "cic:/CoRN/algebra/COrdFields/greater.con" as definition.
 104
 105 (* UNEXPORTED
 106 Implicit Arguments greater [F].
 107 *)
 108
 109 (* NOTATION
 110 Infix "[>]" := greater (at level 70, no associativity).
 111 *)
 112
 113 (* End_SpecReals *)
 114
 115 (*#*
 116 Less or equal is defined as ``not greater than''.
 117 *)
 118
 119 inline procedural "cic:/CoRN/algebra/COrdFields/leEq.con" as definition.
 120
 121 (*#*
 122 %\begin{nameconvention}%
 123 In the names of lemmas, [ [<=] ] is written as [leEq] and
 124 [Zero [<=] ] is written as [nonneg].
 125 %\end{nameconvention}%
 126 *)
 127
 128 (* UNEXPORTED
 129 Implicit Arguments leEq [F].
 130 *)
 131
 132 (* NOTATION
 133 Infix "[<=]" := leEq (at level 70, no associativity).
 134 *)
 135
 136 (* UNEXPORTED
 137 Section COrdField_axioms
 138 *)
 139
 140 (*#*
 141 ** Ordered field axioms
 142 %\begin{convention}%
 143 Let [F] be a field.
 144 %\end{convention}%
 145 *)
 146
 147 (* UNEXPORTED
 148 cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var
 149 *)
 150
 151 inline procedural "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con" as lemma.
 152
 153 inline procedural "cic:/CoRN/algebra/COrdFields/less_strorder.con" as lemma.
 154
 155 inline procedural "cic:/CoRN/algebra/COrdFields/less_transitive_unfolded.con" as lemma.
 156
 157 inline procedural "cic:/CoRN/algebra/COrdFields/less_antisymmetric_unfolded.con" as lemma.
 158
 159 inline procedural "cic:/CoRN/algebra/COrdFields/less_irreflexive.con" as lemma.
 160
 161 inline procedural "cic:/CoRN/algebra/COrdFields/less_irreflexive_unfolded.con" as lemma.
 162
 163 inline procedural "cic:/CoRN/algebra/COrdFields/plus_resp_less_rht.con" as lemma.
 164
 165 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_pos.con" as lemma.
 166
 167 inline procedural "cic:/CoRN/algebra/COrdFields/less_conf_ap.con" as lemma.
 168
 169 inline procedural "cic:/CoRN/algebra/COrdFields/less_wdr.con" as lemma.
 170
 171 inline procedural "cic:/CoRN/algebra/COrdFields/less_wdl.con" as lemma.
 172
 173 (* UNEXPORTED
 174 End COrdField_axioms
 175 *)
 176
 177 (* UNEXPORTED
 178 Declare Left Step less_wdl.
 179 *)
 180
 181 (* UNEXPORTED
 182 Declare Right Step less_wdr.
 183 *)
 184
 185 (* UNEXPORTED
 186 Section OrdField_basics
 187 *)
 188
 189 (*#*
 190 ** Basics
 191 *)
 192
 193 (*#*
 194 %\begin{convention}%
 195 Let in the rest of this section (and all subsections)
 196 [R] be an ordered field
 197 %\end{convention}%
 198 *)
 199
 200 (* UNEXPORTED
 201 cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var
 202 *)
 203
 204 inline procedural "cic:/CoRN/algebra/COrdFields/less_imp_ap.con" as lemma.
 205
 206 inline procedural "cic:/CoRN/algebra/COrdFields/Greater_imp_ap.con" as lemma.
 207
 208 inline procedural "cic:/CoRN/algebra/COrdFields/ap_imp_less.con" as lemma.
 209
 210 (*#*
 211 Now properties which can be derived.
 212 *)
 213
 214 inline procedural "cic:/CoRN/algebra/COrdFields/less_cotransitive.con" as lemma.
 215
 216 inline procedural "cic:/CoRN/algebra/COrdFields/less_cotransitive_unfolded.con" as lemma.
 217
 218 inline procedural "cic:/CoRN/algebra/COrdFields/pos_ap_zero.con" as lemma.
 219
 220 (* Main characterization of less *)
 221
 222 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_not_eq.con" as lemma.
 223
 224 (* UNEXPORTED
 225 End OrdField_basics
 226 *)
 227
 228 (*#**********************************)
 229
 230 (* UNEXPORTED
 231 Section Basic_Properties_of_leEq
 232 *)
 233
 234 (*#**********************************)
 235
 236 (*#* ** Basic properties of [ [<=] ]
 237 *)
 238
 239 (* UNEXPORTED
 240 cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var
 241 *)
 242
 243 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_wdr.con" as lemma.
 244
 245 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_wdl.con" as lemma.
 246
 247 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_reflexive.con" as lemma.
 248
 249 (* UNEXPORTED
 250 Declare Left Step leEq_wdl.
 251 *)
 252
 253 (* UNEXPORTED
 254 Declare Right Step leEq_wdr.
 255 *)
 256
 257 inline procedural "cic:/CoRN/algebra/COrdFields/eq_imp_leEq.con" as lemma.
 258
 259 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_imp_eq.con" as lemma.
 260
 261 inline procedural "cic:/CoRN/algebra/COrdFields/lt_equiv_imp_eq.con" as lemma.
 262
 263 inline procedural "cic:/CoRN/algebra/COrdFields/less_leEq_trans.con" as lemma.
 264
 265 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_less_trans.con" as lemma.
 266
 267 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_transitive.con" as lemma.
 268
 269 inline procedural "cic:/CoRN/algebra/COrdFields/less_leEq.con" as lemma.
 270
 271 (* UNEXPORTED
 272 End Basic_Properties_of_leEq
 273 *)
 274
 275 (* UNEXPORTED
 276 Declare Left Step leEq_wdl.
 277 *)
 278
 279 (* UNEXPORTED
 280 Declare Right Step leEq_wdr.
 281 *)
 282
 283 (* UNEXPORTED
 284 Section infinity_of_cordfields
 285 *)
 286
 287 (*#*
 288 ** Infinity of ordered fields
 289
 290 In an ordered field we have that [One[+]One] and
 291 [One[+]One[+]One] and so on are all apart from zero.
 292 We first show this, so that we can define [TwoNZ], [ThreeNZ]
 293 and so on. These are elements of [NonZeros], so that we can write
 294 e.g.%\% [x[/]TwoNZ].
 295 *)
 296
 297 (* UNEXPORTED
 298 cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var
 299 *)
 300
 301 inline procedural "cic:/CoRN/algebra/COrdFields/pos_one.con" as lemma.
 302
 303 inline procedural "cic:/CoRN/algebra/COrdFields/nring_less_succ.con" as lemma.
 304
 305 inline procedural "cic:/CoRN/algebra/COrdFields/nring_less.con" as lemma.
 306
 307 inline procedural "cic:/CoRN/algebra/COrdFields/nring_leEq.con" as lemma.
 308
 309 inline procedural "cic:/CoRN/algebra/COrdFields/nring_apart.con" as lemma.
 310
 311 inline procedural "cic:/CoRN/algebra/COrdFields/nring_ap_zero.con" as lemma.
 312
 313 inline procedural "cic:/CoRN/algebra/COrdFields/nring_ap_zero'.con" as lemma.
 314
 315 inline procedural "cic:/CoRN/algebra/COrdFields/nring_ap_zero_imp.con" as lemma.
 316
 317 inline procedural "cic:/CoRN/algebra/COrdFields/Snring.con" as definition.
 318
 319 include "tactics/Transparent_algebra.ma".
 320
 321 inline procedural "cic:/CoRN/algebra/COrdFields/pos_Snring.con" as lemma.
 322
 323 inline procedural "cic:/CoRN/algebra/COrdFields/nringS_ap_zero.con" as lemma.
 324
 325 inline procedural "cic:/CoRN/algebra/COrdFields/nring_fac_ap_zero.con" as lemma.
 326
 327 include "tactics/Opaque_algebra.ma".
 328
 329 (* UNEXPORTED
 330 Section up_to_four
 331 *)
 332
 333 (*#*
 334 *** Properties of one up to four
 335 %\begin{nameconvention}%
 336 In the names of lemmas, we denote the numbers 0,1,2,3,4 and so on, by
 337 [zero], [one], [two] etc.
 338 %\end{nameconvention}%
 339 *)
 340
 341 inline procedural "cic:/CoRN/algebra/COrdFields/less_plusOne.con" as lemma.
 342
 343 inline procedural "cic:/CoRN/algebra/COrdFields/zero_lt_posplus1.con" as lemma.
 344
 345 inline procedural "cic:/CoRN/algebra/COrdFields/plus_one_ext_less.con" as lemma.
 346
 347 inline procedural "cic:/CoRN/algebra/COrdFields/one_less_two.con" as lemma.
 348
 349 inline procedural "cic:/CoRN/algebra/COrdFields/two_less_three.con" as lemma.
 350
 351 inline procedural "cic:/CoRN/algebra/COrdFields/three_less_four.con" as lemma.
 352
 353 inline procedural "cic:/CoRN/algebra/COrdFields/pos_two.con" as lemma.
 354
 355 inline procedural "cic:/CoRN/algebra/COrdFields/one_less_three.con" as lemma.
 356
 357 inline procedural "cic:/CoRN/algebra/COrdFields/two_less_four.con" as lemma.
 358
 359 inline procedural "cic:/CoRN/algebra/COrdFields/pos_three.con" as lemma.
 360
 361 inline procedural "cic:/CoRN/algebra/COrdFields/one_less_four.con" as lemma.
 362
 363 inline procedural "cic:/CoRN/algebra/COrdFields/pos_four.con" as lemma.
 364
 365 inline procedural "cic:/CoRN/algebra/COrdFields/two_ap_zero.con" as lemma.
 366
 367 inline procedural "cic:/CoRN/algebra/COrdFields/three_ap_zero.con" as lemma.
 368
 369 inline procedural "cic:/CoRN/algebra/COrdFields/four_ap_zero.con" as lemma.
 370
 371 (* UNEXPORTED
 372 End up_to_four
 373 *)
 374
 375 (* UNEXPORTED
 376 Section More_than_four
 377 *)
 378
 379 (*#* *** Properties of some other numbers *)
 380
 381 inline procedural "cic:/CoRN/algebra/COrdFields/pos_six.con" as lemma.
 382
 383 inline procedural "cic:/CoRN/algebra/COrdFields/pos_eight.con" as lemma.
 384
 385 inline procedural "cic:/CoRN/algebra/COrdFields/pos_nine.con" as lemma.
 386
 387 inline procedural "cic:/CoRN/algebra/COrdFields/pos_twelve.con" as lemma.
 388
 389 inline procedural "cic:/CoRN/algebra/COrdFields/pos_sixteen.con" as lemma.
 390
 391 inline procedural "cic:/CoRN/algebra/COrdFields/pos_eighteen.con" as lemma.
 392
 393 inline procedural "cic:/CoRN/algebra/COrdFields/pos_twentyfour.con" as lemma.
 394
 395 inline procedural "cic:/CoRN/algebra/COrdFields/pos_fortyeight.con" as lemma.
 396
 397 inline procedural "cic:/CoRN/algebra/COrdFields/six_ap_zero.con" as lemma.
 398
 399 inline procedural "cic:/CoRN/algebra/COrdFields/eight_ap_zero.con" as lemma.
 400
 401 inline procedural "cic:/CoRN/algebra/COrdFields/nine_ap_zero.con" as lemma.
 402
 403 inline procedural "cic:/CoRN/algebra/COrdFields/twelve_ap_zero.con" as lemma.
 404
 405 inline procedural "cic:/CoRN/algebra/COrdFields/sixteen_ap_zero.con" as lemma.
 406
 407 inline procedural "cic:/CoRN/algebra/COrdFields/eighteen_ap_zero.con" as lemma.
 408
 409 inline procedural "cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con" as lemma.
 410
 411 inline procedural "cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con" as lemma.
 412
 413 (* UNEXPORTED
 414 End More_than_four
 415 *)
 416
 417 (* UNEXPORTED
 418 End infinity_of_cordfields
 419 *)
 420
 421 (* UNEXPORTED
 422 Declare Left Step leEq_wdl.
 423 *)
 424
 425 (* UNEXPORTED
 426 Declare Right Step leEq_wdr.
 427 *)
 428
 429 (* NOTATION
 430 Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
 431 *)
 432
 433 (* NOTATION
 434 Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
 435 *)
 436
 437 (* NOTATION
 438 Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
 439 *)
 440
 441 (* NOTATION
 442 Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
 443 *)
 444
 445 (* NOTATION
 446 Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
 447 *)
 448
 449 (* NOTATION
 450 Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
 451 *)
 452
 453 (* NOTATION
 454 Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
 455 *)
 456
 457 (* NOTATION
 458 Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
 459 *)
 460
 461 (* NOTATION
 462 Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
 463 *)
 464
 465 (* NOTATION
 466 Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
 467 *)
 468
 469 (* NOTATION
 470 Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
 471 *)
 472
 473 (* NOTATION
 474 Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
 475 *)
 476
 477 (* UNEXPORTED
 478 Section consequences_of_infinity
 479 *)
 480
 481 (*#*
 482 *** Consequences of infinity
 483 *)
 484
 485 (* UNEXPORTED
 486 cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var
 487 *)
 488
 489 inline procedural "cic:/CoRN/algebra/COrdFields/square_eq.con" as lemma.
 490
 491 (*#*
 492 Ordered fields have characteristic zero.
 493 *)
 494
 495 inline procedural "cic:/CoRN/algebra/COrdFields/char0_OrdField.con" as lemma.
 496
 497 (* UNEXPORTED
 498 End consequences_of_infinity
 499 *)
 500
 501 (*#**********************************)
 502
 503 (* UNEXPORTED
 504 Section Properties_of_Ordering
 505 *)
 506
 507 (*#**********************************)
 508
 509 (*#*
 510 ** Properties of [[<]]
 511 *)
 512
 513 (* UNEXPORTED
 514 cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var
 515 *)
 516
 517 (*#*
 518 We do not use a special predicate for positivity,
 519 (e.g.%\% [PosP]), but just write [Zero [<] x].
 520 Reasons: it is more natural; in ordinary mathematics we also write [Zero [<] x]
 521 (or [x [>] Zero]).
 522
 523 *)
 524
 525 (* UNEXPORTED
 526 Section addition
 527 *)
 528
 529 (*#*
 530 *** Addition and subtraction%\label{section:less_plus_minus}%
 531
 532 *)
 533
 534 inline procedural "cic:/CoRN/algebra/COrdFields/plus_resp_less_lft.con" as lemma.
 535
 536 inline procedural "cic:/CoRN/algebra/COrdFields/inv_resp_less.con" as lemma.
 537
 538 (* UNEXPORTED
 539 Transparent cg_minus.
 540 *)
 541
 542 inline procedural "cic:/CoRN/algebra/COrdFields/minus_resp_less.con" as lemma.
 543
 544 (* UNEXPORTED
 545 Transparent cg_minus.
 546 *)
 547
 548 inline procedural "cic:/CoRN/algebra/COrdFields/minus_resp_less_rht.con" as lemma.
 549
 550 inline procedural "cic:/CoRN/algebra/COrdFields/plus_resp_less_both.con" as lemma.
 551
 552 (*#*
 553 For versions of [plus_resp_less_both] where one [ [<] ] in the
 554 assumption is replaced by [ [<=] ]%, see
 555 Section~\ref{section:leEq-plus-minus}%.
 556
 557 Cancellation laws
 558 *)
 559
 560 inline procedural "cic:/CoRN/algebra/COrdFields/plus_cancel_less.con" as lemma.
 561
 562 inline procedural "cic:/CoRN/algebra/COrdFields/inv_cancel_less.con" as lemma.
 563
 564 (*#*
 565
 566 Lemmas where an operation is transformed into the inverse operation on
 567 the other side of an inequality are called laws for shifting.
 568 %\begin{nameconvention}%
 569 The names of laws for shifting start with [shift_], and then come
 570 the operation and the inequality, in the order in which they occur in the
 571 conclusion.
 572 If the shifted operand changes sides w.r.t.%\% the operation and its inverse,
 573 the name gets a prime.
 574 %\end{nameconvention}%
 575
 576 It would be nicer to write the laws for shifting as bi-implications,
 577 However, it is impractical to use these in
 578 Coq%(see the Coq shortcoming in Section~\ref{section:setoid-basics})%.
 579 *)
 580
 581 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_plus.con" as lemma.
 582
 583 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_plus'.con" as lemma.
 584
 585 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_minus.con" as lemma.
 586
 587 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_minus'.con" as lemma.
 588
 589 inline procedural "cic:/CoRN/algebra/COrdFields/shift_plus_less.con" as lemma.
 590
 591 inline procedural "cic:/CoRN/algebra/COrdFields/shift_plus_less'.con" as lemma.
 592
 593 inline procedural "cic:/CoRN/algebra/COrdFields/shift_minus_less.con" as lemma.
 594
 595 inline procedural "cic:/CoRN/algebra/COrdFields/shift_minus_less'.con" as lemma.
 596
 597 (*#*
 598 Some special cases of laws for shifting.
 599 *)
 600
 601 inline procedural "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus.con" as lemma.
 602
 603 inline procedural "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con" as lemma.
 604
 605 inline procedural "cic:/CoRN/algebra/COrdFields/qltone.con" as lemma.
 606
 607 (* UNEXPORTED
 608 End addition
 609 *)
 610
 611 (* UNEXPORTED
 612 Section multiplication
 613 *)
 614
 615 (*#*
 616 *** Multiplication and division
 617 By Convention%~\ref{convention:div-form}%
 618 in CFields% (Section~\ref{section:fields})%, we often have redundant premises
 619 in lemmas. E.g.%\% the informal statement
 620 ``for all [x,y : R] with  [Zero [<] x] and [Zero [<] y]
 621 we have [Zero [<] y[/]x]''
 622 is formalized as follows.
 623 [[
 624 forall (x y : R) x_, (Zero [<] x) -> (Zero [<] y) -> (Zero [<] y[/]x[//]H)
 625 ]]
 626 We do this to keep it easy to use such lemmas.
 627
 628 *)
 629
 630 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_less.con" as lemma.
 631
 632 inline procedural "cic:/CoRN/algebra/COrdFields/recip_resp_pos.con" as lemma.
 633
 634 inline procedural "cic:/CoRN/algebra/COrdFields/div_resp_less_rht.con" as lemma.
 635
 636 inline procedural "cic:/CoRN/algebra/COrdFields/div_resp_pos.con" as lemma.
 637
 638 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_less_lft.con" as lemma.
 639
 640 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_less_both.con" as lemma.
 641
 642 inline procedural "cic:/CoRN/algebra/COrdFields/recip_resp_less.con" as lemma.
 643
 644 inline procedural "cic:/CoRN/algebra/COrdFields/div_resp_less.con" as lemma.
 645
 646 (*#* Cancellation laws
 647 *)
 648
 649 inline procedural "cic:/CoRN/algebra/COrdFields/mult_cancel_less.con" as lemma.
 650
 651 (*#*
 652 Laws for shifting
 653
 654 %For namegiving, see the Section~\ref{section:less_plus_minus}
 655 on plus and minus.%
 656 *)
 657
 658 inline procedural "cic:/CoRN/algebra/COrdFields/shift_div_less.con" as lemma.
 659
 660 inline procedural "cic:/CoRN/algebra/COrdFields/shift_div_less'.con" as lemma.
 661
 662 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_div.con" as lemma.
 663
 664 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_mult.con" as lemma.
 665
 666 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_mult'.con" as lemma.
 667
 668 inline procedural "cic:/CoRN/algebra/COrdFields/shift_mult_less.con" as lemma.
 669
 670 (*#* Other properties of multiplication and division
 671 *)
 672
 673 inline procedural "cic:/CoRN/algebra/COrdFields/minusOne_less.con" as lemma.
 674
 675 inline procedural "cic:/CoRN/algebra/COrdFields/swap_div.con" as lemma.
 676
 677 inline procedural "cic:/CoRN/algebra/COrdFields/eps_div_less_eps.con" as lemma.
 678
 679 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_two.con" as lemma.
 680
 681 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_two'.con" as lemma.
 682
 683 (*
 684 Apply mult_cancel_less with (Two::R).
 685 Apply pos_two.
 686 rstepl eps[+]Zero; rstepr eps[+]eps.
 687 Apply plus_resp_less_lft.
 688 Auto.
 689 Qed.
 690 *)
 691
 692 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_three.con" as lemma.
 693
 694 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_three'.con" as lemma.
 695
 696 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_four.con" as lemma.
 697
 698 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_four'.con" as lemma.
 699
 700 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_six.con" as lemma.
 701
 702 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_eight.con" as lemma.
 703
 704 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_nine.con" as lemma.
 705
 706 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_twelve.con" as lemma.
 707
 708 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_sixteen.con" as lemma.
 709
 710 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_eighteen.con" as lemma.
 711
 712 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con" as lemma.
 713
 714 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con" as lemma.
 715
 716 (* UNEXPORTED
 717 End multiplication
 718 *)
 719
 720 (* UNEXPORTED
 721 Section misc
 722 *)
 723
 724 (*#*
 725 *** Miscellaneous properties
 726 *)
 727
 728 inline procedural "cic:/CoRN/algebra/COrdFields/nring_pos.con" as lemma.
 729
 730 inline procedural "cic:/CoRN/algebra/COrdFields/less_nring.con" as lemma.
 731
 732 inline procedural "cic:/CoRN/algebra/COrdFields/pos_nring_fac.con" as lemma.
 733
 734 inline procedural "cic:/CoRN/algebra/COrdFields/Smallest_less_Average.con" as lemma.
 735
 736 inline procedural "cic:/CoRN/algebra/COrdFields/Average_less_Greatest.con" as lemma.
 737
 738 inline procedural "cic:/CoRN/algebra/COrdFields/Sum_resp_less.con" as lemma.
 739
 740 inline procedural "cic:/CoRN/algebra/COrdFields/Sumx_resp_less.con" as lemma.
 741
 742 inline procedural "cic:/CoRN/algebra/COrdFields/positive_Sum_two.con" as lemma.
 743
 744 inline procedural "cic:/CoRN/algebra/COrdFields/positive_Sumx.con" as lemma.
 745
 746 inline procedural "cic:/CoRN/algebra/COrdFields/negative_Sumx.con" as lemma.
 747
 748 (* UNEXPORTED
 749 End misc
 750 *)
 751
 752 (* UNEXPORTED
 753 End Properties_of_Ordering
 754 *)
 755