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".
19 include "CoRN_notation.ma".
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 inline "cic:/CoRN/algebra/COrdAbs/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.
68 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con".
70 inline "cic:/CoRN/algebra/COrdAbs/zero_AbsSmall.con".
72 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_trans.con".
74 inline "cic:/CoRN/algebra/COrdAbs/leEq_imp_AbsSmall.con".
76 inline "cic:/CoRN/algebra/COrdAbs/inv_resp_AbsSmall.con".
78 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_minus.con".
80 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_plus.con".
82 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div_two.con".
84 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_delta.con".
86 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_delta.con".
88 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_eps_div2.con".
90 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_eps_div2.con".
92 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_intermediate.con".
94 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div2.con".
96 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_nonneg.con".
98 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_mult.con".
100 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_cancel_mult.con".
102 inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_approach_zero.con".
105 End AbsSmall_properties.
109 Declare Left Step AbsSmall_wdl_unfolded.
113 Declare Right Step AbsSmall_wdr_unfolded.
116 (*#* ** Properties of [AbsBig] *)
118 inline "cic:/CoRN/algebra/COrdAbs/absBig.con".
120 inline "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con".
123 Section absBig_wd_properties.
127 %\begin{convention}% Let [R] be an ordered field.
131 inline "cic:/CoRN/algebra/COrdAbs/R.var".
133 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr.con".
135 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl.con".
137 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr_unfolded.con".
139 inline "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl_unfolded.con".
142 End absBig_wd_properties.
146 Declare Left Step AbsBig_wdl_unfolded.
150 Declare Right Step AbsBig_wdr_unfolded.