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