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/COrdFields.ma".
21 (*#* printing one_div_succ %\ensuremath{\frac1{\cdot+1}}% *)
23 (*#* printing Half %\ensuremath{\frac12}% #½# *)
25 (*#**********************************)
28 Section Properties_of_leEq
31 (*#**********************************)
34 ** Properties of [[<=]]
35 %\begin{convention}% Let [R] be an ordered field.
39 alias id "R" = "cic:/CoRN/algebra/COrdFields2/Properties_of_leEq/R.var".
46 *** Addition and subtraction%\label{section:leEq-plus-minus}%
49 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq.con".
51 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_lft.con".
53 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq.con".
55 inline procedural "cic:/CoRN/algebra/COrdFields2/inv_resp_leEq.con".
61 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq_rht.con".
63 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_both.con".
65 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_less_leEq.con".
67 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_less.con".
69 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_less_leEq.con".
71 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq_both.con".
73 (*#* Cancellation properties
76 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_cancel_leEq_rht.con".
78 inline procedural "cic:/CoRN/algebra/COrdFields2/inv_cancel_leEq.con".
80 (*#* Laws for shifting
83 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_plus_leEq.con".
85 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_plus.con".
87 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_plus_leEq'.con".
89 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_plus'.con".
91 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_rht.con".
93 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_lft.con".
95 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_minus_leEq.con".
97 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_minus.con".
99 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_minus'.con".
101 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_zero_leEq_minus.con".
103 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_zero_leEq_minus'.con".
110 Section multiplication
114 *** Multiplication and division
116 Multiplication and division respect [[<=]]
119 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_rht.con".
121 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_lft.con".
123 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_both.con".
125 inline procedural "cic:/CoRN/algebra/COrdFields2/recip_resp_leEq.con".
127 inline procedural "cic:/CoRN/algebra/COrdFields2/div_resp_leEq.con".
130 Hint Resolve recip_resp_leEq: algebra.
133 (*#* Cancellation properties
136 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_cancel_leEq.con".
138 (*#* Laws for shifting
141 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_mult_leEq.con".
143 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_mult_leEq'.con".
145 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_mult'.con".
147 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_div_leEq.con".
149 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_div_leEq'.con".
151 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_div.con".
154 Hint Resolve shift_leEq_div: algebra.
157 inline procedural "cic:/CoRN/algebra/COrdFields2/eps_div_leEq_eps.con".
159 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_two.con".
161 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_two'.con".
163 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_three.con".
165 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_three'.con".
167 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_four.con".
169 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_four'.con".
180 *** Miscellaneous Properties
183 inline procedural "cic:/CoRN/algebra/COrdFields2/sqr_nonneg.con".
185 inline procedural "cic:/CoRN/algebra/COrdFields2/nring_nonneg.con".
187 inline procedural "cic:/CoRN/algebra/COrdFields2/suc_leEq_dub.con".
189 inline procedural "cic:/CoRN/algebra/COrdFields2/leEq_nring.con".
191 inline procedural "cic:/CoRN/algebra/COrdFields2/cc_abs_aid.con".
193 include "tactics/Transparent_algebra.ma".
195 inline procedural "cic:/CoRN/algebra/COrdFields2/nexp_resp_pos.con".
197 include "tactics/Opaque_algebra.ma".
199 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_nonneg.con".
201 include "tactics/Transparent_algebra.ma".
203 inline procedural "cic:/CoRN/algebra/COrdFields2/nexp_resp_nonneg.con".
205 inline procedural "cic:/CoRN/algebra/COrdFields2/power_resp_leEq.con".
207 inline procedural "cic:/CoRN/algebra/COrdFields2/nexp_resp_less.con".
209 inline procedural "cic:/CoRN/algebra/COrdFields2/power_cancel_leEq.con".
211 inline procedural "cic:/CoRN/algebra/COrdFields2/power_cancel_less.con".
213 inline procedural "cic:/CoRN/algebra/COrdFields2/nat_less_bin_nexp.con".
215 inline procedural "cic:/CoRN/algebra/COrdFields2/Sum_resp_leEq.con".
217 inline procedural "cic:/CoRN/algebra/COrdFields2/Sumx_resp_leEq.con".
219 inline procedural "cic:/CoRN/algebra/COrdFields2/Sum2_resp_leEq.con".
221 inline procedural "cic:/CoRN/algebra/COrdFields2/approach_zero.con".
223 inline procedural "cic:/CoRN/algebra/COrdFields2/approach_zero_weak.con".
229 inline procedural "cic:/CoRN/algebra/COrdFields2/equal_less_leEq.con".
232 End Properties_of_leEq
235 (*#**********************************)
238 Section PosP_properties
241 (*#**********************************)
244 ** Properties of positive numbers
245 %\begin{convention}% Let [R] be an ordered field.
249 alias id "R" = "cic:/CoRN/algebra/COrdFields2/PosP_properties/R.var".
254 Notation ZeroR := (Zero:R).
258 Notation OneR := (One:R).
263 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_pos_imp.con".
265 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_pos_nonneg.con".
267 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_nonneg_pos.con".
269 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_square.con".
271 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_cancel_pos_rht.con".
273 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_cancel_pos_lft.con".
275 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_wd.con".
277 inline procedural "cic:/CoRN/algebra/COrdFields2/even_power_pos.con".
279 inline procedural "cic:/CoRN/algebra/COrdFields2/odd_power_cancel_pos.con".
281 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_pos.con".
283 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_nring_S.con".
285 inline procedural "cic:/CoRN/algebra/COrdFields2/square_eq_pos.con".
287 inline procedural "cic:/CoRN/algebra/COrdFields2/square_eq_neg.con".
294 Hint Resolve mult_resp_nonneg.
298 ** Properties of one over successor
299 %\begin{convention}% Let [R] be an ordered field.
303 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ.con".
306 Implicit Arguments one_div_succ [R].
310 Section One_div_succ_properties
313 alias id "R" = "cic:/CoRN/algebra/COrdFields2/One_div_succ_properties/R.var".
315 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_leEq.con".
317 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ_pos.con".
319 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_less.con".
322 End One_div_succ_properties
326 ** Properties of [Half]
329 inline procedural "cic:/CoRN/algebra/COrdFields2/Half.con".
332 Implicit Arguments Half [R].
336 Section Half_properties
341 Let [R] be an ordered field.
345 alias id "R" = "cic:/CoRN/algebra/COrdFields2/Half_properties/R.var".
347 inline procedural "cic:/CoRN/algebra/COrdFields2/half_1.con".
350 Hint Resolve half_1: algebra.
353 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_half.con".
355 inline procedural "cic:/CoRN/algebra/COrdFields2/half_1'.con".
357 inline procedural "cic:/CoRN/algebra/COrdFields2/half_2.con".
359 inline procedural "cic:/CoRN/algebra/COrdFields2/half_lt1.con".
361 inline procedural "cic:/CoRN/algebra/COrdFields2/half_3.con".
368 Hint Resolve half_1 half_1' half_2: algebra.