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.
40 cic:/CoRN/algebra/COrdFields2/Properties_of_leEq/R.var
48 *** Addition and subtraction%\label{section:leEq-plus-minus}%
51 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq.con" as lemma.
53 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_lft.con" as lemma.
55 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq.con" as lemma.
57 inline procedural "cic:/CoRN/algebra/COrdFields2/inv_resp_leEq.con" as lemma.
63 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq_rht.con" as lemma.
65 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_both.con" as lemma.
67 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_less_leEq.con" as lemma.
69 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_leEq_less.con" as lemma.
71 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_less_leEq.con" as lemma.
73 inline procedural "cic:/CoRN/algebra/COrdFields2/minus_resp_leEq_both.con" as lemma.
75 (*#* Cancellation properties
78 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_cancel_leEq_rht.con" as lemma.
80 inline procedural "cic:/CoRN/algebra/COrdFields2/inv_cancel_leEq.con" as lemma.
82 (*#* Laws for shifting
85 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_plus_leEq.con" as lemma.
87 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_plus.con" as lemma.
89 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_plus_leEq'.con" as lemma.
91 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_plus'.con" as lemma.
93 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_rht.con" as lemma.
95 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_lft.con" as lemma.
97 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_minus_leEq.con" as lemma.
99 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_minus.con" as lemma.
101 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_minus'.con" as lemma.
103 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_zero_leEq_minus.con" as lemma.
105 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_zero_leEq_minus'.con" as lemma.
112 Section multiplication
116 *** Multiplication and division
118 Multiplication and division respect [[<=]]
121 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_rht.con" as lemma.
123 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_lft.con" as lemma.
125 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_leEq_both.con" as lemma.
127 inline procedural "cic:/CoRN/algebra/COrdFields2/recip_resp_leEq.con" as lemma.
129 inline procedural "cic:/CoRN/algebra/COrdFields2/div_resp_leEq.con" as lemma.
132 Hint Resolve recip_resp_leEq: algebra.
135 (*#* Cancellation properties
138 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_cancel_leEq.con" as lemma.
140 (*#* Laws for shifting
143 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_mult_leEq.con" as lemma.
145 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_mult_leEq'.con" as lemma.
147 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_mult'.con" as lemma.
149 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_div_leEq.con" as lemma.
151 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_div_leEq'.con" as lemma.
153 inline procedural "cic:/CoRN/algebra/COrdFields2/shift_leEq_div.con" as lemma.
156 Hint Resolve shift_leEq_div: algebra.
159 inline procedural "cic:/CoRN/algebra/COrdFields2/eps_div_leEq_eps.con" as lemma.
161 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_two.con" as lemma.
163 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_two'.con" as lemma.
165 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_three.con" as lemma.
167 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_three'.con" as lemma.
169 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_four.con" as lemma.
171 inline procedural "cic:/CoRN/algebra/COrdFields2/nonneg_div_four'.con" as lemma.
182 *** Miscellaneous Properties
185 inline procedural "cic:/CoRN/algebra/COrdFields2/sqr_nonneg.con" as lemma.
187 inline procedural "cic:/CoRN/algebra/COrdFields2/nring_nonneg.con" as lemma.
189 inline procedural "cic:/CoRN/algebra/COrdFields2/suc_leEq_dub.con" as lemma.
191 inline procedural "cic:/CoRN/algebra/COrdFields2/leEq_nring.con" as lemma.
193 inline procedural "cic:/CoRN/algebra/COrdFields2/cc_abs_aid.con" as lemma.
195 include "tactics/Transparent_algebra.ma".
197 inline procedural "cic:/CoRN/algebra/COrdFields2/nexp_resp_pos.con" as lemma.
199 include "tactics/Opaque_algebra.ma".
201 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_resp_nonneg.con" as lemma.
203 include "tactics/Transparent_algebra.ma".
205 inline procedural "cic:/CoRN/algebra/COrdFields2/nexp_resp_nonneg.con" as lemma.
207 inline procedural "cic:/CoRN/algebra/COrdFields2/power_resp_leEq.con" as lemma.
209 inline procedural "cic:/CoRN/algebra/COrdFields2/nexp_resp_less.con" as lemma.
211 inline procedural "cic:/CoRN/algebra/COrdFields2/power_cancel_leEq.con" as lemma.
213 inline procedural "cic:/CoRN/algebra/COrdFields2/power_cancel_less.con" as lemma.
215 inline procedural "cic:/CoRN/algebra/COrdFields2/nat_less_bin_nexp.con" as lemma.
217 inline procedural "cic:/CoRN/algebra/COrdFields2/Sum_resp_leEq.con" as lemma.
219 inline procedural "cic:/CoRN/algebra/COrdFields2/Sumx_resp_leEq.con" as lemma.
221 inline procedural "cic:/CoRN/algebra/COrdFields2/Sum2_resp_leEq.con" as lemma.
223 inline procedural "cic:/CoRN/algebra/COrdFields2/approach_zero.con" as lemma.
225 inline procedural "cic:/CoRN/algebra/COrdFields2/approach_zero_weak.con" as lemma.
231 inline procedural "cic:/CoRN/algebra/COrdFields2/equal_less_leEq.con" as lemma.
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.
252 cic:/CoRN/algebra/COrdFields2/PosP_properties/R.var
258 Notation ZeroR := (Zero:R).
262 Notation OneR := (One:R).
267 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_pos_imp.con" as lemma.
269 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_pos_nonneg.con" as lemma.
271 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_nonneg_pos.con" as lemma.
273 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_square.con" as lemma.
275 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_cancel_pos_rht.con" as lemma.
277 inline procedural "cic:/CoRN/algebra/COrdFields2/mult_cancel_pos_lft.con" as lemma.
279 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_wd.con" as lemma.
281 inline procedural "cic:/CoRN/algebra/COrdFields2/even_power_pos.con" as lemma.
283 inline procedural "cic:/CoRN/algebra/COrdFields2/odd_power_cancel_pos.con" as lemma.
285 inline procedural "cic:/CoRN/algebra/COrdFields2/plus_resp_pos.con" as lemma.
287 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_nring_S.con" as lemma.
289 inline procedural "cic:/CoRN/algebra/COrdFields2/square_eq_pos.con" as lemma.
291 inline procedural "cic:/CoRN/algebra/COrdFields2/square_eq_neg.con" as lemma.
298 Hint Resolve mult_resp_nonneg.
302 ** Properties of one over successor
303 %\begin{convention}% Let [R] be an ordered field.
307 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ.con" as definition.
310 Implicit Arguments one_div_succ [R].
314 Section One_div_succ_properties
318 cic:/CoRN/algebra/COrdFields2/One_div_succ_properties/R.var
321 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_leEq.con" as lemma.
323 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ_pos.con" as lemma.
325 inline procedural "cic:/CoRN/algebra/COrdFields2/one_div_succ_resp_less.con" as lemma.
328 End One_div_succ_properties
332 ** Properties of [Half]
335 inline procedural "cic:/CoRN/algebra/COrdFields2/Half.con" as definition.
338 Implicit Arguments Half [R].
342 Section Half_properties
347 Let [R] be an ordered field.
352 cic:/CoRN/algebra/COrdFields2/Half_properties/R.var
355 inline procedural "cic:/CoRN/algebra/COrdFields2/half_1.con" as lemma.
358 Hint Resolve half_1: algebra.
361 inline procedural "cic:/CoRN/algebra/COrdFields2/pos_half.con" as lemma.
363 inline procedural "cic:/CoRN/algebra/COrdFields2/half_1'.con" as lemma.
365 inline procedural "cic:/CoRN/algebra/COrdFields2/half_2.con" as lemma.
367 inline procedural "cic:/CoRN/algebra/COrdFields2/half_lt1.con" as lemma.
369 inline procedural "cic:/CoRN/algebra/COrdFields2/half_3.con" as lemma.
376 Hint Resolve half_1 half_1' half_2: algebra.