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 *********************)
19 include "algebra/COrdFields2.ma".
22 ** Properties of [AbsSmall]
27 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall.con".
30 Implicit Arguments AbsSmall [R].
36 Section AbsSmall_properties
40 %\begin{convention}% Let [R] be an ordered field.
44 alias id "R" = "cic:/CoRN/algebra/COrdAbs/AbsSmall_properties/R.var".
46 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdr.con".
48 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdr_unfolded.con".
50 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdl.con".
52 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdl_unfolded.con".
55 Declare Left Step AbsSmall_wdl_unfolded.
59 Declare Right Step AbsSmall_wdr_unfolded.
65 Notation ZeroR := (Zero:R).
70 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con".
72 inline procedural "cic:/CoRN/algebra/COrdAbs/zero_AbsSmall.con".
74 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_trans.con".
76 inline procedural "cic:/CoRN/algebra/COrdAbs/leEq_imp_AbsSmall.con".
78 inline procedural "cic:/CoRN/algebra/COrdAbs/inv_resp_AbsSmall.con".
80 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_minus.con".
82 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_plus.con".
84 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div_two.con".
86 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_delta.con".
88 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_delta.con".
90 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_eps_div2.con".
92 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_eps_div2.con".
94 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_intermediate.con".
96 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div2.con".
98 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_nonneg.con".
100 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_mult.con".
102 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_cancel_mult.con".
104 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_approach_zero.con".
107 End AbsSmall_properties
111 Declare Left Step AbsSmall_wdl_unfolded.
115 Declare Right Step AbsSmall_wdr_unfolded.
118 (*#* ** Properties of [AbsBig] *)
120 inline procedural "cic:/CoRN/algebra/COrdAbs/absBig.con".
123 Notation AbsBig := (absBig _).
126 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con".
129 Section absBig_wd_properties
133 %\begin{convention}% Let [R] be an ordered field.
137 alias id "R" = "cic:/CoRN/algebra/COrdAbs/absBig_wd_properties/R.var".
139 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr.con".
141 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl.con".
143 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr_unfolded.con".
145 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl_unfolded.con".
148 End absBig_wd_properties
152 Declare Left Step AbsBig_wdl_unfolded.
156 Declare Right Step AbsBig_wdr_unfolded.