X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCOrdFields.ma;h=cb6476676c55a1c0cbd2aaf1f4d37fe88d19f37b;hb=f2d9db85559c7a8db11aae1153495fae4a258d54;hp=69382e44fa761af6dde13cd849b782c4956fc136;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma index 69382e44f..cb6476676 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields". +include "CoRN.ma". + (* $Id: COrdFields.v,v 1.6 2004/04/23 10:00:52 lcf Exp $ *) (*#* printing [<] %\ensuremath<% #<# *) @@ -48,9 +50,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields". (*#* printing FortyEightNZ %\ensuremath{\mathbf{48}}% #48# *) -(* INCLUDE -FieldReflection -*) +include "tactics/FieldReflection.ma". (* ORDERED FIELDS *) @@ -61,7 +61,7 @@ FieldReflection (* Begin_SpecReals *) -inline cic:/CoRN/algebra/COrdFields/strictorder.ind. +inline "cic:/CoRN/algebra/COrdFields/strictorder.ind". (* UNEXPORTED Implicit Arguments strictorder [A]. @@ -79,9 +79,11 @@ Implicit Arguments so_trans [A R]. Implicit Arguments so_asym [A R]. *) -inline cic:/CoRN/algebra/COrdFields/is_COrdField.ind. +inline "cic:/CoRN/algebra/COrdFields/is_COrdField.ind". + +inline "cic:/CoRN/algebra/COrdFields/COrdField.ind". -inline cic:/CoRN/algebra/COrdFields/COrdField.ind. +coercion cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con 0 (* compounds *). (*#* %\begin{nameconvention}% @@ -94,19 +96,27 @@ is written as [pos]. Implicit Arguments cof_less [c]. *) -inline cic:/CoRN/algebra/COrdFields/greater.con. +(* NOTATION +Infix "[<]" := cof_less (at level 70, no associativity). +*) + +inline "cic:/CoRN/algebra/COrdFields/greater.con". (* UNEXPORTED Implicit Arguments greater [F]. *) +(* NOTATION +Infix "[>]" := greater (at level 70, no associativity). +*) + (* End_SpecReals *) (*#* Less or equal is defined as ``not greater than''. *) -inline cic:/CoRN/algebra/COrdFields/leEq.con. +inline "cic:/CoRN/algebra/COrdFields/leEq.con". (*#* %\begin{nameconvention}% @@ -119,8 +129,12 @@ In the names of lemmas, [ [<=] ] is written as [leEq] and Implicit Arguments leEq [F]. *) +(* NOTATION +Infix "[<=]" := leEq (at level 70, no associativity). +*) + (* UNEXPORTED -Section COrdField_axioms. +Section COrdField_axioms *) (*#* @@ -130,32 +144,32 @@ Let [F] be a field. %\end{convention}% *) -inline cic:/CoRN/algebra/COrdFields/F.var. +alias id "F" = "cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var". -inline cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con. +inline "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con". -inline cic:/CoRN/algebra/COrdFields/less_strorder.con. +inline "cic:/CoRN/algebra/COrdFields/less_strorder.con". -inline cic:/CoRN/algebra/COrdFields/less_transitive_unfolded.con. +inline "cic:/CoRN/algebra/COrdFields/less_transitive_unfolded.con". -inline cic:/CoRN/algebra/COrdFields/less_antisymmetric_unfolded.con. +inline "cic:/CoRN/algebra/COrdFields/less_antisymmetric_unfolded.con". -inline cic:/CoRN/algebra/COrdFields/less_irreflexive.con. +inline "cic:/CoRN/algebra/COrdFields/less_irreflexive.con". -inline cic:/CoRN/algebra/COrdFields/less_irreflexive_unfolded.con. +inline "cic:/CoRN/algebra/COrdFields/less_irreflexive_unfolded.con". -inline cic:/CoRN/algebra/COrdFields/plus_resp_less_rht.con. +inline "cic:/CoRN/algebra/COrdFields/plus_resp_less_rht.con". -inline cic:/CoRN/algebra/COrdFields/mult_resp_pos.con. +inline "cic:/CoRN/algebra/COrdFields/mult_resp_pos.con". -inline cic:/CoRN/algebra/COrdFields/less_conf_ap.con. +inline "cic:/CoRN/algebra/COrdFields/less_conf_ap.con". -inline cic:/CoRN/algebra/COrdFields/less_wdr.con. +inline "cic:/CoRN/algebra/COrdFields/less_wdr.con". -inline cic:/CoRN/algebra/COrdFields/less_wdl.con. +inline "cic:/CoRN/algebra/COrdFields/less_wdl.con". (* UNEXPORTED -End COrdField_axioms. +End COrdField_axioms *) (* UNEXPORTED @@ -167,7 +181,7 @@ Declare Right Step less_wdr. *) (* UNEXPORTED -Section OrdField_basics. +Section OrdField_basics *) (*#* @@ -181,36 +195,36 @@ Let in the rest of this section (and all subsections) %\end{convention}% *) -inline cic:/CoRN/algebra/COrdFields/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var". -inline cic:/CoRN/algebra/COrdFields/less_imp_ap.con. +inline "cic:/CoRN/algebra/COrdFields/less_imp_ap.con". -inline cic:/CoRN/algebra/COrdFields/Greater_imp_ap.con. +inline "cic:/CoRN/algebra/COrdFields/Greater_imp_ap.con". -inline cic:/CoRN/algebra/COrdFields/ap_imp_less.con. +inline "cic:/CoRN/algebra/COrdFields/ap_imp_less.con". (*#* Now properties which can be derived. *) -inline cic:/CoRN/algebra/COrdFields/less_cotransitive.con. +inline "cic:/CoRN/algebra/COrdFields/less_cotransitive.con". -inline cic:/CoRN/algebra/COrdFields/less_cotransitive_unfolded.con. +inline "cic:/CoRN/algebra/COrdFields/less_cotransitive_unfolded.con". -inline cic:/CoRN/algebra/COrdFields/pos_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/pos_ap_zero.con". (* Main characterization of less *) -inline cic:/CoRN/algebra/COrdFields/leEq_not_eq.con. +inline "cic:/CoRN/algebra/COrdFields/leEq_not_eq.con". (* UNEXPORTED -End OrdField_basics. +End OrdField_basics *) (*#**********************************) (* UNEXPORTED -Section Basic_Properties_of_leEq. +Section Basic_Properties_of_leEq *) (*#**********************************) @@ -218,13 +232,13 @@ Section Basic_Properties_of_leEq. (*#* ** Basic properties of [ [<=] ] *) -inline cic:/CoRN/algebra/COrdFields/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var". -inline cic:/CoRN/algebra/COrdFields/leEq_wdr.con. +inline "cic:/CoRN/algebra/COrdFields/leEq_wdr.con". -inline cic:/CoRN/algebra/COrdFields/leEq_wdl.con. +inline "cic:/CoRN/algebra/COrdFields/leEq_wdl.con". -inline cic:/CoRN/algebra/COrdFields/leEq_reflexive.con. +inline "cic:/CoRN/algebra/COrdFields/leEq_reflexive.con". (* UNEXPORTED Declare Left Step leEq_wdl. @@ -234,22 +248,22 @@ Declare Left Step leEq_wdl. Declare Right Step leEq_wdr. *) -inline cic:/CoRN/algebra/COrdFields/eq_imp_leEq.con. +inline "cic:/CoRN/algebra/COrdFields/eq_imp_leEq.con". -inline cic:/CoRN/algebra/COrdFields/leEq_imp_eq.con. +inline "cic:/CoRN/algebra/COrdFields/leEq_imp_eq.con". -inline cic:/CoRN/algebra/COrdFields/lt_equiv_imp_eq.con. +inline "cic:/CoRN/algebra/COrdFields/lt_equiv_imp_eq.con". -inline cic:/CoRN/algebra/COrdFields/less_leEq_trans.con. +inline "cic:/CoRN/algebra/COrdFields/less_leEq_trans.con". -inline cic:/CoRN/algebra/COrdFields/leEq_less_trans.con. +inline "cic:/CoRN/algebra/COrdFields/leEq_less_trans.con". -inline cic:/CoRN/algebra/COrdFields/leEq_transitive.con. +inline "cic:/CoRN/algebra/COrdFields/leEq_transitive.con". -inline cic:/CoRN/algebra/COrdFields/less_leEq.con. +inline "cic:/CoRN/algebra/COrdFields/less_leEq.con". (* UNEXPORTED -End Basic_Properties_of_leEq. +End Basic_Properties_of_leEq *) (* UNEXPORTED @@ -261,7 +275,7 @@ Declare Right Step leEq_wdr. *) (* UNEXPORTED -Section infinity_of_cordfields. +Section infinity_of_cordfields *) (*#* @@ -274,42 +288,38 @@ and so on. These are elements of [NonZeros], so that we can write e.g.%\% [x[/]TwoNZ]. *) -inline cic:/CoRN/algebra/COrdFields/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var". -inline cic:/CoRN/algebra/COrdFields/pos_one.con. +inline "cic:/CoRN/algebra/COrdFields/pos_one.con". -inline cic:/CoRN/algebra/COrdFields/nring_less_succ.con. +inline "cic:/CoRN/algebra/COrdFields/nring_less_succ.con". -inline cic:/CoRN/algebra/COrdFields/nring_less.con. +inline "cic:/CoRN/algebra/COrdFields/nring_less.con". -inline cic:/CoRN/algebra/COrdFields/nring_leEq.con. +inline "cic:/CoRN/algebra/COrdFields/nring_leEq.con". -inline cic:/CoRN/algebra/COrdFields/nring_apart.con. +inline "cic:/CoRN/algebra/COrdFields/nring_apart.con". -inline cic:/CoRN/algebra/COrdFields/nring_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/nring_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/nring_ap_zero'.con. +inline "cic:/CoRN/algebra/COrdFields/nring_ap_zero'.con". -inline cic:/CoRN/algebra/COrdFields/nring_ap_zero_imp.con. +inline "cic:/CoRN/algebra/COrdFields/nring_ap_zero_imp.con". -inline cic:/CoRN/algebra/COrdFields/Snring.con. +inline "cic:/CoRN/algebra/COrdFields/Snring.con". -(* INCLUDE -Transparent_algebra -*) +include "tactics/Transparent_algebra.ma". -inline cic:/CoRN/algebra/COrdFields/pos_Snring.con. +inline "cic:/CoRN/algebra/COrdFields/pos_Snring.con". -inline cic:/CoRN/algebra/COrdFields/nringS_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/nringS_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/nring_fac_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/nring_fac_ap_zero.con". -(* INCLUDE -Opaque_algebra -*) +include "tactics/Opaque_algebra.ma". (* UNEXPORTED -Section up_to_four. +Section up_to_four *) (*#* @@ -320,84 +330,84 @@ In the names of lemmas, we denote the numbers 0,1,2,3,4 and so on, by %\end{nameconvention}% *) -inline cic:/CoRN/algebra/COrdFields/less_plusOne.con. +inline "cic:/CoRN/algebra/COrdFields/less_plusOne.con". -inline cic:/CoRN/algebra/COrdFields/zero_lt_posplus1.con. +inline "cic:/CoRN/algebra/COrdFields/zero_lt_posplus1.con". -inline cic:/CoRN/algebra/COrdFields/plus_one_ext_less.con. +inline "cic:/CoRN/algebra/COrdFields/plus_one_ext_less.con". -inline cic:/CoRN/algebra/COrdFields/one_less_two.con. +inline "cic:/CoRN/algebra/COrdFields/one_less_two.con". -inline cic:/CoRN/algebra/COrdFields/two_less_three.con. +inline "cic:/CoRN/algebra/COrdFields/two_less_three.con". -inline cic:/CoRN/algebra/COrdFields/three_less_four.con. +inline "cic:/CoRN/algebra/COrdFields/three_less_four.con". -inline cic:/CoRN/algebra/COrdFields/pos_two.con. +inline "cic:/CoRN/algebra/COrdFields/pos_two.con". -inline cic:/CoRN/algebra/COrdFields/one_less_three.con. +inline "cic:/CoRN/algebra/COrdFields/one_less_three.con". -inline cic:/CoRN/algebra/COrdFields/two_less_four.con. +inline "cic:/CoRN/algebra/COrdFields/two_less_four.con". -inline cic:/CoRN/algebra/COrdFields/pos_three.con. +inline "cic:/CoRN/algebra/COrdFields/pos_three.con". -inline cic:/CoRN/algebra/COrdFields/one_less_four.con. +inline "cic:/CoRN/algebra/COrdFields/one_less_four.con". -inline cic:/CoRN/algebra/COrdFields/pos_four.con. +inline "cic:/CoRN/algebra/COrdFields/pos_four.con". -inline cic:/CoRN/algebra/COrdFields/two_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/two_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/three_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/three_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/four_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/four_ap_zero.con". (* UNEXPORTED -End up_to_four. +End up_to_four *) (* UNEXPORTED -Section More_than_four. +Section More_than_four *) (*#* *** Properties of some other numbers *) -inline cic:/CoRN/algebra/COrdFields/pos_six.con. +inline "cic:/CoRN/algebra/COrdFields/pos_six.con". -inline cic:/CoRN/algebra/COrdFields/pos_eight.con. +inline "cic:/CoRN/algebra/COrdFields/pos_eight.con". -inline cic:/CoRN/algebra/COrdFields/pos_nine.con. +inline "cic:/CoRN/algebra/COrdFields/pos_nine.con". -inline cic:/CoRN/algebra/COrdFields/pos_twelve.con. +inline "cic:/CoRN/algebra/COrdFields/pos_twelve.con". -inline cic:/CoRN/algebra/COrdFields/pos_sixteen.con. +inline "cic:/CoRN/algebra/COrdFields/pos_sixteen.con". -inline cic:/CoRN/algebra/COrdFields/pos_eighteen.con. +inline "cic:/CoRN/algebra/COrdFields/pos_eighteen.con". -inline cic:/CoRN/algebra/COrdFields/pos_twentyfour.con. +inline "cic:/CoRN/algebra/COrdFields/pos_twentyfour.con". -inline cic:/CoRN/algebra/COrdFields/pos_fortyeight.con. +inline "cic:/CoRN/algebra/COrdFields/pos_fortyeight.con". -inline cic:/CoRN/algebra/COrdFields/six_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/six_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/eight_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/eight_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/nine_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/nine_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/twelve_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/twelve_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/sixteen_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/sixteen_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/eighteen_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/eighteen_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con". -inline cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con. +inline "cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con". (* UNEXPORTED -End More_than_four. +End More_than_four *) (* UNEXPORTED -End infinity_of_cordfields. +End infinity_of_cordfields *) (* UNEXPORTED @@ -408,32 +418,80 @@ Declare Left Step leEq_wdl. Declare Right Step leEq_wdr. *) +(* NOTATION +Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20). +*) + (* UNEXPORTED -Section consequences_of_infinity. +Section consequences_of_infinity *) (*#* *** Consequences of infinity *) -inline cic:/CoRN/algebra/COrdFields/F.var. +alias id "F" = "cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var". -inline cic:/CoRN/algebra/COrdFields/square_eq.con. +inline "cic:/CoRN/algebra/COrdFields/square_eq.con". (*#* Ordered fields have characteristic zero. *) -inline cic:/CoRN/algebra/COrdFields/char0_OrdField.con. +inline "cic:/CoRN/algebra/COrdFields/char0_OrdField.con". (* UNEXPORTED -End consequences_of_infinity. +End consequences_of_infinity *) (*#**********************************) (* UNEXPORTED -Section Properties_of_Ordering. +Section Properties_of_Ordering *) (*#**********************************) @@ -442,7 +500,7 @@ Section Properties_of_Ordering. ** Properties of [[<]] *) -inline cic:/CoRN/algebra/COrdFields/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var". (*#* We do not use a special predicate for positivity, @@ -453,7 +511,7 @@ Reasons: it is more natural; in ordinary mathematics we also write [Zero [<] x] *) (* UNEXPORTED -Section addition. +Section addition *) (*#* @@ -461,23 +519,23 @@ Section addition. *) -inline cic:/CoRN/algebra/COrdFields/plus_resp_less_lft.con. +inline "cic:/CoRN/algebra/COrdFields/plus_resp_less_lft.con". -inline cic:/CoRN/algebra/COrdFields/inv_resp_less.con. +inline "cic:/CoRN/algebra/COrdFields/inv_resp_less.con". (* UNEXPORTED Transparent cg_minus. *) -inline cic:/CoRN/algebra/COrdFields/minus_resp_less.con. +inline "cic:/CoRN/algebra/COrdFields/minus_resp_less.con". (* UNEXPORTED Transparent cg_minus. *) -inline cic:/CoRN/algebra/COrdFields/minus_resp_less_rht.con. +inline "cic:/CoRN/algebra/COrdFields/minus_resp_less_rht.con". -inline cic:/CoRN/algebra/COrdFields/plus_resp_less_both.con. +inline "cic:/CoRN/algebra/COrdFields/plus_resp_less_both.con". (*#* For versions of [plus_resp_less_both] where one [ [<] ] in the @@ -487,9 +545,9 @@ Section~\ref{section:leEq-plus-minus}%. Cancellation laws *) -inline cic:/CoRN/algebra/COrdFields/plus_cancel_less.con. +inline "cic:/CoRN/algebra/COrdFields/plus_cancel_less.con". -inline cic:/CoRN/algebra/COrdFields/inv_cancel_less.con. +inline "cic:/CoRN/algebra/COrdFields/inv_cancel_less.con". (*#* @@ -508,38 +566,38 @@ However, it is impractical to use these in Coq%(see the Coq shortcoming in Section~\ref{section:setoid-basics})%. *) -inline cic:/CoRN/algebra/COrdFields/shift_less_plus.con. +inline "cic:/CoRN/algebra/COrdFields/shift_less_plus.con". -inline cic:/CoRN/algebra/COrdFields/shift_less_plus'.con. +inline "cic:/CoRN/algebra/COrdFields/shift_less_plus'.con". -inline cic:/CoRN/algebra/COrdFields/shift_less_minus.con. +inline "cic:/CoRN/algebra/COrdFields/shift_less_minus.con". -inline cic:/CoRN/algebra/COrdFields/shift_less_minus'.con. +inline "cic:/CoRN/algebra/COrdFields/shift_less_minus'.con". -inline cic:/CoRN/algebra/COrdFields/shift_plus_less.con. +inline "cic:/CoRN/algebra/COrdFields/shift_plus_less.con". -inline cic:/CoRN/algebra/COrdFields/shift_plus_less'.con. +inline "cic:/CoRN/algebra/COrdFields/shift_plus_less'.con". -inline cic:/CoRN/algebra/COrdFields/shift_minus_less.con. +inline "cic:/CoRN/algebra/COrdFields/shift_minus_less.con". -inline cic:/CoRN/algebra/COrdFields/shift_minus_less'.con. +inline "cic:/CoRN/algebra/COrdFields/shift_minus_less'.con". (*#* Some special cases of laws for shifting. *) -inline cic:/CoRN/algebra/COrdFields/shift_zero_less_minus.con. +inline "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus.con". -inline cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con. +inline "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con". -inline cic:/CoRN/algebra/COrdFields/qltone.con. +inline "cic:/CoRN/algebra/COrdFields/qltone.con". (* UNEXPORTED -End addition. +End addition *) (* UNEXPORTED -Section multiplication. +Section multiplication *) (*#* @@ -557,26 +615,26 @@ We do this to keep it easy to use such lemmas. *) -inline cic:/CoRN/algebra/COrdFields/mult_resp_less.con. +inline "cic:/CoRN/algebra/COrdFields/mult_resp_less.con". -inline cic:/CoRN/algebra/COrdFields/recip_resp_pos.con. +inline "cic:/CoRN/algebra/COrdFields/recip_resp_pos.con". -inline cic:/CoRN/algebra/COrdFields/div_resp_less_rht.con. +inline "cic:/CoRN/algebra/COrdFields/div_resp_less_rht.con". -inline cic:/CoRN/algebra/COrdFields/div_resp_pos.con. +inline "cic:/CoRN/algebra/COrdFields/div_resp_pos.con". -inline cic:/CoRN/algebra/COrdFields/mult_resp_less_lft.con. +inline "cic:/CoRN/algebra/COrdFields/mult_resp_less_lft.con". -inline cic:/CoRN/algebra/COrdFields/mult_resp_less_both.con. +inline "cic:/CoRN/algebra/COrdFields/mult_resp_less_both.con". -inline cic:/CoRN/algebra/COrdFields/recip_resp_less.con. +inline "cic:/CoRN/algebra/COrdFields/recip_resp_less.con". -inline cic:/CoRN/algebra/COrdFields/div_resp_less.con. +inline "cic:/CoRN/algebra/COrdFields/div_resp_less.con". (*#* Cancellation laws *) -inline cic:/CoRN/algebra/COrdFields/mult_cancel_less.con. +inline "cic:/CoRN/algebra/COrdFields/mult_cancel_less.con". (*#* Laws for shifting @@ -585,30 +643,30 @@ Laws for shifting on plus and minus.% *) -inline cic:/CoRN/algebra/COrdFields/shift_div_less.con. +inline "cic:/CoRN/algebra/COrdFields/shift_div_less.con". -inline cic:/CoRN/algebra/COrdFields/shift_div_less'.con. +inline "cic:/CoRN/algebra/COrdFields/shift_div_less'.con". -inline cic:/CoRN/algebra/COrdFields/shift_less_div.con. +inline "cic:/CoRN/algebra/COrdFields/shift_less_div.con". -inline cic:/CoRN/algebra/COrdFields/shift_less_mult.con. +inline "cic:/CoRN/algebra/COrdFields/shift_less_mult.con". -inline cic:/CoRN/algebra/COrdFields/shift_less_mult'.con. +inline "cic:/CoRN/algebra/COrdFields/shift_less_mult'.con". -inline cic:/CoRN/algebra/COrdFields/shift_mult_less.con. +inline "cic:/CoRN/algebra/COrdFields/shift_mult_less.con". (*#* Other properties of multiplication and division *) -inline cic:/CoRN/algebra/COrdFields/minusOne_less.con. +inline "cic:/CoRN/algebra/COrdFields/minusOne_less.con". -inline cic:/CoRN/algebra/COrdFields/swap_div.con. +inline "cic:/CoRN/algebra/COrdFields/swap_div.con". -inline cic:/CoRN/algebra/COrdFields/eps_div_less_eps.con. +inline "cic:/CoRN/algebra/COrdFields/eps_div_less_eps.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_two.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_two.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_two'.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_two'.con". (* Apply mult_cancel_less with (Two::R). @@ -619,67 +677,67 @@ Auto. Qed. *) -inline cic:/CoRN/algebra/COrdFields/pos_div_three.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_three.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_three'.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_three'.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_four.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_four.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_four'.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_four'.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_six.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_six.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_eight.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_eight.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_nine.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_nine.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_twelve.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_twelve.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_sixteen.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_sixteen.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_eighteen.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_eighteen.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con". -inline cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con. +inline "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con". (* UNEXPORTED -End multiplication. +End multiplication *) (* UNEXPORTED -Section misc. +Section misc *) (*#* *** Miscellaneous properties *) -inline cic:/CoRN/algebra/COrdFields/nring_pos.con. +inline "cic:/CoRN/algebra/COrdFields/nring_pos.con". -inline cic:/CoRN/algebra/COrdFields/less_nring.con. +inline "cic:/CoRN/algebra/COrdFields/less_nring.con". -inline cic:/CoRN/algebra/COrdFields/pos_nring_fac.con. +inline "cic:/CoRN/algebra/COrdFields/pos_nring_fac.con". -inline cic:/CoRN/algebra/COrdFields/Smallest_less_Average.con. +inline "cic:/CoRN/algebra/COrdFields/Smallest_less_Average.con". -inline cic:/CoRN/algebra/COrdFields/Average_less_Greatest.con. +inline "cic:/CoRN/algebra/COrdFields/Average_less_Greatest.con". -inline cic:/CoRN/algebra/COrdFields/Sum_resp_less.con. +inline "cic:/CoRN/algebra/COrdFields/Sum_resp_less.con". -inline cic:/CoRN/algebra/COrdFields/Sumx_resp_less.con. +inline "cic:/CoRN/algebra/COrdFields/Sumx_resp_less.con". -inline cic:/CoRN/algebra/COrdFields/positive_Sum_two.con. +inline "cic:/CoRN/algebra/COrdFields/positive_Sum_two.con". -inline cic:/CoRN/algebra/COrdFields/positive_Sumx.con. +inline "cic:/CoRN/algebra/COrdFields/positive_Sumx.con". -inline cic:/CoRN/algebra/COrdFields/negative_Sumx.con. +inline "cic:/CoRN/algebra/COrdFields/negative_Sumx.con". (* UNEXPORTED -End misc. +End misc *) (* UNEXPORTED -End Properties_of_Ordering. +End Properties_of_Ordering *)