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