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/COrdFields2".
21 include "algebra/COrdFields.ma".
23 (*#* printing one_div_succ %\ensuremath{\frac1{\cdot+1}}% *)
25 (*#* printing Half %\ensuremath{\frac12}% #½# *)
27 (*#**********************************)
30 Section Properties_of_leEq
33 (*#**********************************)
36 ** Properties of [[<=]]
37 %\begin{convention}% Let [R] be an ordered field.
41 alias id "R" = "cic:/CoRN/algebra/COrdFields2/Properties_of_leEq/R.var".
48 *** Addition and subtraction%\label{section:leEq-plus-minus}%
51 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq.con".
53 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_lft.con".
55 inline "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq.con".
57 inline "cic:/CoRN/algebra/COrdFields2/inv_resp_leEq.con".
63 inline "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq_rht.con".
65 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_both.con".
67 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_less_leEq.con".
69 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_less.con".
71 inline "cic:/CoRN/algebra/COrdFields2/minus_resp_less_leEq.con".
73 inline "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq_both.con".
75 (*#* Cancellation properties
78 inline "cic:/CoRN/algebra/COrdFields2/plus_cancel_leEq_rht.con".
80 inline "cic:/CoRN/algebra/COrdFields2/inv_cancel_leEq.con".
82 (*#* Laws for shifting
85 inline "cic:/CoRN/algebra/COrdFields2/shift_plus_leEq.con".
87 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_plus.con".
89 inline "cic:/CoRN/algebra/COrdFields2/shift_plus_leEq'.con".
91 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_plus'.con".
93 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_rht.con".
95 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_lft.con".
97 inline "cic:/CoRN/algebra/COrdFields2/shift_minus_leEq.con".
99 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_minus.con".
101 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_minus'.con".
103 inline "cic:/CoRN/algebra/COrdFields2/shift_zero_leEq_minus.con".
105 inline "cic:/CoRN/algebra/COrdFields2/shift_zero_leEq_minus'.con".
112 Section multiplication
116 *** Multiplication and division
118 Multiplication and division respect [[<=]]
121 inline "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_rht.con".
123 inline "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_lft.con".
125 inline "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_both.con".
127 inline "cic:/CoRN/algebra/COrdFields2/recip_resp_leEq.con".
129 inline "cic:/CoRN/algebra/COrdFields2/div_resp_leEq.con".
132 Hint Resolve recip_resp_leEq: algebra.
135 (*#* Cancellation properties
138 inline "cic:/CoRN/algebra/COrdFields2/mult_cancel_leEq.con".
140 (*#* Laws for shifting
143 inline "cic:/CoRN/algebra/COrdFields2/shift_mult_leEq.con".
145 inline "cic:/CoRN/algebra/COrdFields2/shift_mult_leEq'.con".
147 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_mult'.con".
149 inline "cic:/CoRN/algebra/COrdFields2/shift_div_leEq.con".
151 inline "cic:/CoRN/algebra/COrdFields2/shift_div_leEq'.con".
153 inline "cic:/CoRN/algebra/COrdFields2/shift_leEq_div.con".
156 Hint Resolve shift_leEq_div: algebra.
159 inline "cic:/CoRN/algebra/COrdFields2/eps_div_leEq_eps.con".
161 inline "cic:/CoRN/algebra/COrdFields2/nonneg_div_two.con".
163 inline "cic:/CoRN/algebra/COrdFields2/nonneg_div_two'.con".
165 inline "cic:/CoRN/algebra/COrdFields2/nonneg_div_three.con".
167 inline "cic:/CoRN/algebra/COrdFields2/nonneg_div_three'.con".
169 inline "cic:/CoRN/algebra/COrdFields2/nonneg_div_four.con".
171 inline "cic:/CoRN/algebra/COrdFields2/nonneg_div_four'.con".
182 *** Miscellaneous Properties
185 inline "cic:/CoRN/algebra/COrdFields2/sqr_nonneg.con".
187 inline "cic:/CoRN/algebra/COrdFields2/nring_nonneg.con".
189 inline "cic:/CoRN/algebra/COrdFields2/suc_leEq_dub.con".
191 inline "cic:/CoRN/algebra/COrdFields2/leEq_nring.con".
193 inline "cic:/CoRN/algebra/COrdFields2/cc_abs_aid.con".
195 include "tactics/Transparent_algebra.ma".
197 inline "cic:/CoRN/algebra/COrdFields2/nexp_resp_pos.con".
199 include "tactics/Opaque_algebra.ma".
201 inline "cic:/CoRN/algebra/COrdFields2/mult_resp_nonneg.con".
203 include "tactics/Transparent_algebra.ma".
205 inline "cic:/CoRN/algebra/COrdFields2/nexp_resp_nonneg.con".
207 inline "cic:/CoRN/algebra/COrdFields2/power_resp_leEq.con".
209 inline "cic:/CoRN/algebra/COrdFields2/nexp_resp_less.con".
211 inline "cic:/CoRN/algebra/COrdFields2/power_cancel_leEq.con".
213 inline "cic:/CoRN/algebra/COrdFields2/power_cancel_less.con".
215 inline "cic:/CoRN/algebra/COrdFields2/nat_less_bin_nexp.con".
217 inline "cic:/CoRN/algebra/COrdFields2/Sum_resp_leEq.con".
219 inline "cic:/CoRN/algebra/COrdFields2/Sumx_resp_leEq.con".
221 inline "cic:/CoRN/algebra/COrdFields2/Sum2_resp_leEq.con".
223 inline "cic:/CoRN/algebra/COrdFields2/approach_zero.con".
225 inline "cic:/CoRN/algebra/COrdFields2/approach_zero_weak.con".
231 inline "cic:/CoRN/algebra/COrdFields2/equal_less_leEq.con".
234 End Properties_of_leEq
237 (*#**********************************)
240 Section PosP_properties
243 (*#**********************************)
246 ** Properties of positive numbers
247 %\begin{convention}% Let [R] be an ordered field.
251 alias id "R" = "cic:/CoRN/algebra/COrdFields2/PosP_properties/R.var".
256 Notation ZeroR := (Zero:R).
260 Notation OneR := (One:R).
265 inline "cic:/CoRN/algebra/COrdFields2/mult_pos_imp.con".
267 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_pos_nonneg.con".
269 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_nonneg_pos.con".
271 inline "cic:/CoRN/algebra/COrdFields2/pos_square.con".
273 inline "cic:/CoRN/algebra/COrdFields2/mult_cancel_pos_rht.con".
275 inline "cic:/CoRN/algebra/COrdFields2/mult_cancel_pos_lft.con".
277 inline "cic:/CoRN/algebra/COrdFields2/pos_wd.con".
279 inline "cic:/CoRN/algebra/COrdFields2/even_power_pos.con".
281 inline "cic:/CoRN/algebra/COrdFields2/odd_power_cancel_pos.con".
283 inline "cic:/CoRN/algebra/COrdFields2/plus_resp_pos.con".
285 inline "cic:/CoRN/algebra/COrdFields2/pos_nring_S.con".
287 inline "cic:/CoRN/algebra/COrdFields2/square_eq_pos.con".
289 inline "cic:/CoRN/algebra/COrdFields2/square_eq_neg.con".
296 Hint Resolve mult_resp_nonneg.
300 ** Properties of one over successor
301 %\begin{convention}% Let [R] be an ordered field.
305 inline "cic:/CoRN/algebra/COrdFields2/one_div_succ.con".
308 Implicit Arguments one_div_succ [R].
312 Section One_div_succ_properties
315 alias id "R" = "cic:/CoRN/algebra/COrdFields2/One_div_succ_properties/R.var".
317 inline "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_leEq.con".
319 inline "cic:/CoRN/algebra/COrdFields2/one_div_succ_pos.con".
321 inline "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_less.con".
324 End One_div_succ_properties
328 ** Properties of [Half]
331 inline "cic:/CoRN/algebra/COrdFields2/Half.con".
334 Implicit Arguments Half [R].
338 Section Half_properties
343 Let [R] be an ordered field.
347 alias id "R" = "cic:/CoRN/algebra/COrdFields2/Half_properties/R.var".
349 inline "cic:/CoRN/algebra/COrdFields2/half_1.con".
352 Hint Resolve half_1: algebra.
355 inline "cic:/CoRN/algebra/COrdFields2/pos_half.con".
357 inline "cic:/CoRN/algebra/COrdFields2/half_1'.con".
359 inline "cic:/CoRN/algebra/COrdFields2/half_2.con".
361 inline "cic:/CoRN/algebra/COrdFields2/half_lt1.con".
363 inline "cic:/CoRN/algebra/COrdFields2/half_3.con".
370 Hint Resolve half_1 half_1' half_2: algebra.