matita/contribs/CoRN-Decl/algebra/COrdFields.ma

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