1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdAbs".
21 include "algebra/COrdFields2.ma".
24 ** Properties of [AbsSmall]
29 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall.con".
32 Implicit Arguments AbsSmall [R].
38 Section AbsSmall_properties
42 %\begin{convention}% Let [R] be an ordered field.
46 alias id "R" = "cic:/CoRN/algebra/COrdAbs/AbsSmall_properties/R.var".
48 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdr.con".
50 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdr_unfolded.con".
52 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdl.con".
54 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdl_unfolded.con".
57 Declare Left Step AbsSmall_wdl_unfolded.
61 Declare Right Step AbsSmall_wdr_unfolded.
67 Notation ZeroR := (Zero:R).
72 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con".
74 inline "cic:/CoRN/algebra/COrdAbs/zero_AbsSmall.con".
76 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_trans.con".
78 inline "cic:/CoRN/algebra/COrdAbs/leEq_imp_AbsSmall.con".
80 inline "cic:/CoRN/algebra/COrdAbs/inv_resp_AbsSmall.con".
82 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_minus.con".
84 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_plus.con".
86 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div_two.con".
88 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_delta.con".
90 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_delta.con".
92 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_eps_div2.con".
94 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_eps_div2.con".
96 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_intermediate.con".
98 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div2.con".
100 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_nonneg.con".
102 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_mult.con".
104 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_cancel_mult.con".
106 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_approach_zero.con".
109 End AbsSmall_properties
113 Declare Left Step AbsSmall_wdl_unfolded.
117 Declare Right Step AbsSmall_wdr_unfolded.
120 (*#* ** Properties of [AbsBig] *)
122 inline "cic:/CoRN/algebra/COrdAbs/absBig.con".
125 Notation AbsBig := (absBig _).
128 inline "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con".
131 Section absBig_wd_properties
135 %\begin{convention}% Let [R] be an ordered field.
139 alias id "R" = "cic:/CoRN/algebra/COrdAbs/absBig_wd_properties/R.var".
141 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr.con".
143 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl.con".
145 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr_unfolded.con".
147 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl_unfolded.con".
150 End absBig_wd_properties
154 Declare Left Step AbsBig_wdl_unfolded.
158 Declare Right Step AbsBig_wdr_unfolded.