]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/Coq/Reals/RIneq.mma
df90c5f04d3a396f2e54cb56121e4a72926b8be6
[helm.git] / helm / software / matita / contribs / procedural / Coq / Reals / RIneq.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "Coq.ma".
18
19 (*#**********************************************************************)
20
21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
22
23 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
24
25 (*   \VV/  *************************************************************)
26
27 (*    //   *      This file is distributed under the terms of the      *)
28
29 (*         *       GNU Lesser General Public License Version 2.1       *)
30
31 (*#**********************************************************************)
32
33 (*i $Id: RIneq.v,v 1.23 2003/12/15 19:48:20 barras Exp $ i*)
34
35 (*#**************************************************************************)
36
37 (*#*              Basic lemmas for the classical reals numbers              *)
38
39 (*#**************************************************************************)
40
41 include "Reals/Raxioms.ma".
42
43 (* UNEXPORTED
44 Open Local Scope Z_scope.
45 *)
46
47 (* UNEXPORTED
48 Open Local Scope R_scope.
49 *)
50
51 (* UNEXPORTED
52 Implicit Type r : R.
53 *)
54
55 (*#**************************************************************************)
56
57 (*#*       Instantiating Ring tactic on reals                               *)
58
59 (*#**************************************************************************)
60
61 inline procedural "cic:/Coq/Reals/RIneq/RTheory.con" as lemma.
62
63 (* NOTATION
64 Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
65  with minus := Rminus div := Rdiv.
66 *)
67
68 (*#*************************************************************************)
69
70 (*#*  Relation between orders and equality                                 *)
71
72 (*#*************************************************************************)
73
74 (*#*********)
75
76 inline procedural "cic:/Coq/Reals/RIneq/Rlt_irrefl.con" as lemma.
77
78 (* UNEXPORTED
79 Hint Resolve Rlt_irrefl: real.
80 *)
81
82 inline procedural "cic:/Coq/Reals/RIneq/Rle_refl.con" as lemma.
83
84 inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_eq.con" as lemma.
85
86 inline procedural "cic:/Coq/Reals/RIneq/Rgt_not_eq.con" as lemma.
87
88 (*#*********)
89
90 inline procedural "cic:/Coq/Reals/RIneq/Rlt_dichotomy_converse.con" as lemma.
91
92 (* UNEXPORTED
93 Hint Resolve Rlt_dichotomy_converse: real.
94 *)
95
96 (*#* Reasoning by case on equalities and order *)
97
98 (*#*********)
99
100 inline procedural "cic:/Coq/Reals/RIneq/Req_dec.con" as lemma.
101
102 (* UNEXPORTED
103 Hint Resolve Req_dec: real.
104 *)
105
106 (*#*********)
107
108 inline procedural "cic:/Coq/Reals/RIneq/Rtotal_order.con" as lemma.
109
110 (*#*********)
111
112 inline procedural "cic:/Coq/Reals/RIneq/Rdichotomy.con" as lemma.
113
114 (*#********************************************************************************)
115
116 (*#*       Order Lemma  : relating [<], [>], [<=] and [>=]                       *)
117
118 (*#********************************************************************************)
119
120 (*#*********)
121
122 inline procedural "cic:/Coq/Reals/RIneq/Rlt_le.con" as lemma.
123
124 (* UNEXPORTED
125 Hint Resolve Rlt_le: real.
126 *)
127
128 (*#*********)
129
130 inline procedural "cic:/Coq/Reals/RIneq/Rle_ge.con" as lemma.
131
132 (* UNEXPORTED
133 Hint Immediate Rle_ge: real.
134 *)
135
136 (*#*********)
137
138 inline procedural "cic:/Coq/Reals/RIneq/Rge_le.con" as lemma.
139
140 (* UNEXPORTED
141 Hint Resolve Rge_le: real.
142 *)
143
144 (*#*********)
145
146 inline procedural "cic:/Coq/Reals/RIneq/Rnot_le_lt.con" as lemma.
147
148 (* UNEXPORTED
149 Hint Immediate Rnot_le_lt: real.
150 *)
151
152 inline procedural "cic:/Coq/Reals/RIneq/Rnot_ge_lt.con" as lemma.
153
154 (*#*********)
155
156 inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_le.con" as lemma.
157
158 inline procedural "cic:/Coq/Reals/RIneq/Rgt_not_le.con" as lemma.
159
160 (* UNEXPORTED
161 Hint Immediate Rlt_not_le: real.
162 *)
163
164 inline procedural "cic:/Coq/Reals/RIneq/Rle_not_lt.con" as lemma.
165
166 (*#*********)
167
168 inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_ge.con" as lemma.
169
170 (* UNEXPORTED
171 Hint Immediate Rlt_not_ge: real.
172 *)
173
174 (*#*********)
175
176 inline procedural "cic:/Coq/Reals/RIneq/Req_le.con" as lemma.
177
178 (* UNEXPORTED
179 Hint Immediate Req_le: real.
180 *)
181
182 inline procedural "cic:/Coq/Reals/RIneq/Req_ge.con" as lemma.
183
184 (* UNEXPORTED
185 Hint Immediate Req_ge: real.
186 *)
187
188 inline procedural "cic:/Coq/Reals/RIneq/Req_le_sym.con" as lemma.
189
190 (* UNEXPORTED
191 Hint Immediate Req_le_sym: real.
192 *)
193
194 inline procedural "cic:/Coq/Reals/RIneq/Req_ge_sym.con" as lemma.
195
196 (* UNEXPORTED
197 Hint Immediate Req_ge_sym: real.
198 *)
199
200 inline procedural "cic:/Coq/Reals/RIneq/Rle_antisym.con" as lemma.
201
202 (* UNEXPORTED
203 Hint Resolve Rle_antisym: real.
204 *)
205
206 (*#*********)
207
208 inline procedural "cic:/Coq/Reals/RIneq/Rle_le_eq.con" as lemma.
209
210 inline procedural "cic:/Coq/Reals/RIneq/Rlt_eq_compat.con" as lemma.
211
212 (*#*********)
213
214 inline procedural "cic:/Coq/Reals/RIneq/Rle_trans.con" as lemma.
215
216 (*#*********)
217
218 inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_trans.con" as lemma.
219
220 (*#*********)
221
222 inline procedural "cic:/Coq/Reals/RIneq/Rlt_le_trans.con" as lemma.
223
224 (*#* Decidability of the order *)
225
226 inline procedural "cic:/Coq/Reals/RIneq/Rlt_dec.con" as lemma.
227
228 (*#*********)
229
230 inline procedural "cic:/Coq/Reals/RIneq/Rle_dec.con" as lemma.
231
232 (*#*********)
233
234 inline procedural "cic:/Coq/Reals/RIneq/Rgt_dec.con" as lemma.
235
236 (*#*********)
237
238 inline procedural "cic:/Coq/Reals/RIneq/Rge_dec.con" as lemma.
239
240 inline procedural "cic:/Coq/Reals/RIneq/Rlt_le_dec.con" as lemma.
241
242 inline procedural "cic:/Coq/Reals/RIneq/Rle_or_lt.con" as lemma.
243
244 inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_or_eq_dec.con" as lemma.
245
246 (*#*********)
247
248 inline procedural "cic:/Coq/Reals/RIneq/inser_trans_R.con" as lemma.
249
250 (*#***************************************************************)
251
252 (*#*        Field Lemmas                                         *)
253
254 (* This part contains lemma involving the Fields operations     *)
255
256 (*#***************************************************************)
257
258 (*#********************************************************)
259
260 (*#*      Addition                                        *)
261
262 (*#********************************************************)
263
264 inline procedural "cic:/Coq/Reals/RIneq/Rplus_ne.con" as lemma.
265
266 (* UNEXPORTED
267 Hint Resolve Rplus_ne: real v62.
268 *)
269
270 inline procedural "cic:/Coq/Reals/RIneq/Rplus_0_r.con" as lemma.
271
272 (* UNEXPORTED
273 Hint Resolve Rplus_0_r: real.
274 *)
275
276 (*#*********)
277
278 inline procedural "cic:/Coq/Reals/RIneq/Rplus_opp_l.con" as lemma.
279
280 (* UNEXPORTED
281 Hint Resolve Rplus_opp_l: real.
282 *)
283
284 (*#*********)
285
286 inline procedural "cic:/Coq/Reals/RIneq/Rplus_opp_r_uniq.con" as lemma.
287
288 (*i New i*)
289
290 (* UNEXPORTED
291 Hint Resolve (f_equal (A:=R)): real.
292 *)
293
294 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_compat_l.con" as lemma.
295
296 (*i Old i*)
297
298 (* UNEXPORTED
299 Hint Resolve Rplus_eq_compat_l: v62.
300 *)
301
302 (*#*********)
303
304 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_reg_l.con" as lemma.
305
306 (* UNEXPORTED
307 Hint Resolve Rplus_eq_reg_l: real.
308 *)
309
310 (*#*********)
311
312 inline procedural "cic:/Coq/Reals/RIneq/Rplus_0_r_uniq.con" as lemma.
313
314 (*#**********************************************************)
315
316 (*#*       Multiplication                                   *)
317
318 (*#**********************************************************)
319
320 (*#*********)
321
322 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r.con" as lemma.
323
324 (* UNEXPORTED
325 Hint Resolve Rinv_r: real.
326 *)
327
328 inline procedural "cic:/Coq/Reals/RIneq/Rinv_l_sym.con" as lemma.
329
330 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_sym.con" as lemma.
331
332 (* UNEXPORTED
333 Hint Resolve Rinv_l_sym Rinv_r_sym: real.
334 *)
335
336 (*#*********)
337
338 inline procedural "cic:/Coq/Reals/RIneq/Rmult_0_r.con" as lemma.
339
340 (* UNEXPORTED
341 Hint Resolve Rmult_0_r: real v62.
342 *)
343
344 (*#*********)
345
346 inline procedural "cic:/Coq/Reals/RIneq/Rmult_0_l.con" as lemma.
347
348 (* UNEXPORTED
349 Hint Resolve Rmult_0_l: real v62.
350 *)
351
352 (*#*********)
353
354 inline procedural "cic:/Coq/Reals/RIneq/Rmult_ne.con" as lemma.
355
356 (* UNEXPORTED
357 Hint Resolve Rmult_ne: real v62.
358 *)
359
360 (*#*********)
361
362 inline procedural "cic:/Coq/Reals/RIneq/Rmult_1_r.con" as lemma.
363
364 (* UNEXPORTED
365 Hint Resolve Rmult_1_r: real.
366 *)
367
368 (*#*********)
369
370 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_compat_l.con" as lemma.
371
372 (*i OLD i*)
373
374 (* UNEXPORTED
375 Hint Resolve Rmult_eq_compat_l: v62.
376 *)
377
378 (*#*********)
379
380 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_reg_l.con" as lemma.
381
382 (*#*********)
383
384 inline procedural "cic:/Coq/Reals/RIneq/Rmult_integral.con" as lemma.
385
386 (*#*********)
387
388 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat.con" as lemma.
389
390 (* UNEXPORTED
391 Hint Resolve Rmult_eq_0_compat: real.
392 *)
393
394 (*#*********)
395
396 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_r.con" as lemma.
397
398 (*#*********)
399
400 inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_l.con" as lemma.
401
402 (*#*********)
403
404 inline procedural "cic:/Coq/Reals/RIneq/Rmult_neq_0_reg.con" as lemma.
405
406 (*#*********)
407
408 inline procedural "cic:/Coq/Reals/RIneq/Rmult_integral_contrapositive.con" as lemma.
409
410 (* UNEXPORTED
411 Hint Resolve Rmult_integral_contrapositive: real.
412 *)
413
414 (*#*********)
415
416 inline procedural "cic:/Coq/Reals/RIneq/Rmult_plus_distr_r.con" as lemma.
417
418 (*#* Square function *)
419
420 (*#**********)
421
422 inline procedural "cic:/Coq/Reals/RIneq/Rsqr.con" as definition.
423
424 (*#**********)
425
426 inline procedural "cic:/Coq/Reals/RIneq/Rsqr_0.con" as lemma.
427
428 (*#**********)
429
430 inline procedural "cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con" as lemma.
431
432 (*#********************************************************)
433
434 (*#*      Opposite                                        *)
435
436 (*#********************************************************)
437
438 (*#*********)
439
440 inline procedural "cic:/Coq/Reals/RIneq/Ropp_eq_compat.con" as lemma.
441
442 (* UNEXPORTED
443 Hint Resolve Ropp_eq_compat: real.
444 *)
445
446 (*#*********)
447
448 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0.con" as lemma.
449
450 (* UNEXPORTED
451 Hint Resolve Ropp_0: real v62.
452 *)
453
454 (*#*********)
455
456 inline procedural "cic:/Coq/Reals/RIneq/Ropp_eq_0_compat.con" as lemma.
457
458 (* UNEXPORTED
459 Hint Resolve Ropp_eq_0_compat: real.
460 *)
461
462 (*#*********)
463
464 inline procedural "cic:/Coq/Reals/RIneq/Ropp_involutive.con" as lemma.
465
466 (* UNEXPORTED
467 Hint Resolve Ropp_involutive: real.
468 *)
469
470 (*#********)
471
472 inline procedural "cic:/Coq/Reals/RIneq/Ropp_neq_0_compat.con" as lemma.
473
474 (* UNEXPORTED
475 Hint Resolve Ropp_neq_0_compat: real.
476 *)
477
478 (*#*********)
479
480 inline procedural "cic:/Coq/Reals/RIneq/Ropp_plus_distr.con" as lemma.
481
482 (* UNEXPORTED
483 Hint Resolve Ropp_plus_distr: real.
484 *)
485
486 (*#* Opposite and multiplication *)
487
488 inline procedural "cic:/Coq/Reals/RIneq/Ropp_mult_distr_l_reverse.con" as lemma.
489
490 (* UNEXPORTED
491 Hint Resolve Ropp_mult_distr_l_reverse: real.
492 *)
493
494 (*#*********)
495
496 inline procedural "cic:/Coq/Reals/RIneq/Rmult_opp_opp.con" as lemma.
497
498 (* UNEXPORTED
499 Hint Resolve Rmult_opp_opp: real.
500 *)
501
502 inline procedural "cic:/Coq/Reals/RIneq/Ropp_mult_distr_r_reverse.con" as lemma.
503
504 (*#* Substraction *)
505
506 inline procedural "cic:/Coq/Reals/RIneq/Rminus_0_r.con" as lemma.
507
508 (* UNEXPORTED
509 Hint Resolve Rminus_0_r: real.
510 *)
511
512 inline procedural "cic:/Coq/Reals/RIneq/Rminus_0_l.con" as lemma.
513
514 (* UNEXPORTED
515 Hint Resolve Rminus_0_l: real.
516 *)
517
518 (*#*********)
519
520 inline procedural "cic:/Coq/Reals/RIneq/Ropp_minus_distr.con" as lemma.
521
522 (* UNEXPORTED
523 Hint Resolve Ropp_minus_distr: real.
524 *)
525
526 inline procedural "cic:/Coq/Reals/RIneq/Ropp_minus_distr'.con" as lemma.
527
528 (* UNEXPORTED
529 Hint Resolve Ropp_minus_distr': real.
530 *)
531
532 (*#*********)
533
534 inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_eq.con" as lemma.
535
536 (* UNEXPORTED
537 Hint Resolve Rminus_diag_eq: real.
538 *)
539
540 (*#*********)
541
542 inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_uniq.con" as lemma.
543
544 (* UNEXPORTED
545 Hint Immediate Rminus_diag_uniq: real.
546 *)
547
548 inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_uniq_sym.con" as lemma.
549
550 (* UNEXPORTED
551 Hint Immediate Rminus_diag_uniq_sym: real.
552 *)
553
554 inline procedural "cic:/Coq/Reals/RIneq/Rplus_minus.con" as lemma.
555
556 (* UNEXPORTED
557 Hint Resolve Rplus_minus: real.
558 *)
559
560 (*#*********)
561
562 inline procedural "cic:/Coq/Reals/RIneq/Rminus_eq_contra.con" as lemma.
563
564 (* UNEXPORTED
565 Hint Resolve Rminus_eq_contra: real.
566 *)
567
568 inline procedural "cic:/Coq/Reals/RIneq/Rminus_not_eq.con" as lemma.
569
570 (* UNEXPORTED
571 Hint Resolve Rminus_not_eq: real.
572 *)
573
574 inline procedural "cic:/Coq/Reals/RIneq/Rminus_not_eq_right.con" as lemma.
575
576 (* UNEXPORTED
577 Hint Resolve Rminus_not_eq_right: real.
578 *)
579
580 (*#*********)
581
582 inline procedural "cic:/Coq/Reals/RIneq/Rmult_minus_distr_l.con" as lemma.
583
584 (*#* Inverse *)
585
586 inline procedural "cic:/Coq/Reals/RIneq/Rinv_1.con" as lemma.
587
588 (* UNEXPORTED
589 Hint Resolve Rinv_1: real.
590 *)
591
592 (*#********)
593
594 inline procedural "cic:/Coq/Reals/RIneq/Rinv_neq_0_compat.con" as lemma.
595
596 (* UNEXPORTED
597 Hint Resolve Rinv_neq_0_compat: real.
598 *)
599
600 (*#********)
601
602 inline procedural "cic:/Coq/Reals/RIneq/Rinv_involutive.con" as lemma.
603
604 (* UNEXPORTED
605 Hint Resolve Rinv_involutive: real.
606 *)
607
608 (*#********)
609
610 inline procedural "cic:/Coq/Reals/RIneq/Rinv_mult_distr.con" as lemma.
611
612 (*#********)
613
614 inline procedural "cic:/Coq/Reals/RIneq/Ropp_inv_permute.con" as lemma.
615
616 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_r.con" as lemma.
617
618 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_l.con" as lemma.
619
620 inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_m.con" as lemma.
621
622 (* UNEXPORTED
623 Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real.
624 *)
625
626 (*#********)
627
628 inline procedural "cic:/Coq/Reals/RIneq/Rinv_mult_simpl.con" as lemma.
629
630 (*#* Order and addition *)
631
632 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_compat_r.con" as lemma.
633
634 (* UNEXPORTED
635 Hint Resolve Rplus_lt_compat_r: real.
636 *)
637
638 (*#*********)
639
640 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_reg_r.con" as lemma.
641
642 (*#*********)
643
644 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat_l.con" as lemma.
645
646 (*#*********)
647
648 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat_r.con" as lemma.
649
650 (* UNEXPORTED
651 Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.
652 *)
653
654 (*#*********)
655
656 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_reg_l.con" as lemma.
657
658 (*#*********)
659
660 inline procedural "cic:/Coq/Reals/RIneq/sum_inequa_Rle_lt.con" as lemma.
661
662 (*#********)
663
664 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_compat.con" as lemma.
665
666 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat.con" as lemma.
667
668 (*#********)
669
670 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_le_compat.con" as lemma.
671
672 (*#********)
673
674 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_lt_compat.con" as lemma.
675
676 (* UNEXPORTED
677 Hint Immediate Rplus_lt_compat Rplus_le_compat Rplus_lt_le_compat
678   Rplus_le_lt_compat: real.
679 *)
680
681 (*#* Order and Opposite *)
682
683 (*#*********)
684
685 inline procedural "cic:/Coq/Reals/RIneq/Ropp_gt_lt_contravar.con" as lemma.
686
687 (* UNEXPORTED
688 Hint Resolve Ropp_gt_lt_contravar.
689 *)
690
691 (*#*********)
692
693 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_gt_contravar.con" as lemma.
694
695 (* UNEXPORTED
696 Hint Resolve Ropp_lt_gt_contravar: real.
697 *)
698
699 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_cancel.con" as lemma.
700
701 (* UNEXPORTED
702 Hint Immediate Ropp_lt_cancel: real.
703 *)
704
705 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_contravar.con" as lemma.
706
707 (* UNEXPORTED
708 Hint Resolve Ropp_lt_contravar: real.
709 *)
710
711 (*#*********)
712
713 inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_ge_contravar.con" as lemma.
714
715 (* UNEXPORTED
716 Hint Resolve Ropp_le_ge_contravar: real.
717 *)
718
719 inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_cancel.con" as lemma.
720
721 (* UNEXPORTED
722 Hint Immediate Ropp_le_cancel: real.
723 *)
724
725 inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_contravar.con" as lemma.
726
727 (* UNEXPORTED
728 Hint Resolve Ropp_le_contravar: real.
729 *)
730
731 (*#*********)
732
733 inline procedural "cic:/Coq/Reals/RIneq/Ropp_ge_le_contravar.con" as lemma.
734
735 (* UNEXPORTED
736 Hint Resolve Ropp_ge_le_contravar: real.
737 *)
738
739 (*#*********)
740
741 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_lt_gt_contravar.con" as lemma.
742
743 (* UNEXPORTED
744 Hint Resolve Ropp_0_lt_gt_contravar: real.
745 *)
746
747 (*#*********)
748
749 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_gt_lt_contravar.con" as lemma.
750
751 (* UNEXPORTED
752 Hint Resolve Ropp_0_gt_lt_contravar: real.
753 *)
754
755 (*#*********)
756
757 inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_gt_0_contravar.con" as lemma.
758
759 (*#*********)
760
761 inline procedural "cic:/Coq/Reals/RIneq/Ropp_gt_lt_0_contravar.con" as lemma.
762
763 (* UNEXPORTED
764 Hint Resolve Ropp_lt_gt_0_contravar Ropp_gt_lt_0_contravar: real.
765 *)
766
767 (*#*********)
768
769 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_le_ge_contravar.con" as lemma.
770
771 (* UNEXPORTED
772 Hint Resolve Ropp_0_le_ge_contravar: real.
773 *)
774
775 (*#*********)
776
777 inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_ge_le_contravar.con" as lemma.
778
779 (* UNEXPORTED
780 Hint Resolve Ropp_0_ge_le_contravar: real.
781 *)
782
783 (*#* Order and multiplication *)
784
785 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_compat_r.con" as lemma.
786
787 (* UNEXPORTED
788 Hint Resolve Rmult_lt_compat_r.
789 *)
790
791 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_reg_l.con" as lemma.
792
793 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_gt_compat_neg_l.con" as lemma.
794
795 (*#*********)
796
797 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_l.con" as lemma.
798
799 (* UNEXPORTED
800 Hint Resolve Rmult_le_compat_l: real.
801 *)
802
803 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_r.con" as lemma.
804
805 (* UNEXPORTED
806 Hint Resolve Rmult_le_compat_r: real.
807 *)
808
809 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_reg_l.con" as lemma.
810
811 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_neg_l.con" as lemma.
812
813 (* UNEXPORTED
814 Hint Resolve Rmult_le_compat_neg_l: real.
815 *)
816
817 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_ge_compat_neg_l.con" as lemma.
818
819 (* UNEXPORTED
820 Hint Resolve Rmult_le_ge_compat_neg_l: real.
821 *)
822
823 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat.con" as lemma.
824
825 (* UNEXPORTED
826 Hint Resolve Rmult_le_compat: real.
827 *)
828
829 inline procedural "cic:/Coq/Reals/RIneq/Rmult_gt_0_lt_compat.con" as lemma.
830
831 (*#********)
832
833 inline procedural "cic:/Coq/Reals/RIneq/Rmult_ge_0_gt_0_lt_compat.con" as lemma.
834
835 (*#* Order and Substractions *)
836
837 inline procedural "cic:/Coq/Reals/RIneq/Rlt_minus.con" as lemma.
838
839 (* UNEXPORTED
840 Hint Resolve Rlt_minus: real.
841 *)
842
843 (*#*********)
844
845 inline procedural "cic:/Coq/Reals/RIneq/Rle_minus.con" as lemma.
846
847 (*#*********)
848
849 inline procedural "cic:/Coq/Reals/RIneq/Rminus_lt.con" as lemma.
850
851 (*#*********)
852
853 inline procedural "cic:/Coq/Reals/RIneq/Rminus_le.con" as lemma.
854
855 (*#*********)
856
857 inline procedural "cic:/Coq/Reals/RIneq/tech_Rplus.con" as lemma.
858
859 (* UNEXPORTED
860 Hint Immediate tech_Rplus: real.
861 *)
862
863 (*#* Order and the square function *)
864
865 inline procedural "cic:/Coq/Reals/RIneq/Rle_0_sqr.con" as lemma.
866
867 (*#**********)
868
869 inline procedural "cic:/Coq/Reals/RIneq/Rlt_0_sqr.con" as lemma.
870
871 (* UNEXPORTED
872 Hint Resolve Rle_0_sqr Rlt_0_sqr: real.
873 *)
874
875 (*#* Zero is less than one *)
876
877 inline procedural "cic:/Coq/Reals/RIneq/Rlt_0_1.con" as lemma.
878
879 (* UNEXPORTED
880 Hint Resolve Rlt_0_1: real.
881 *)
882
883 inline procedural "cic:/Coq/Reals/RIneq/Rle_0_1.con" as lemma.
884
885 (*#* Order and inverse *)
886
887 inline procedural "cic:/Coq/Reals/RIneq/Rinv_0_lt_compat.con" as lemma.
888
889 (* UNEXPORTED
890 Hint Resolve Rinv_0_lt_compat: real.
891 *)
892
893 (*#********)
894
895 inline procedural "cic:/Coq/Reals/RIneq/Rinv_lt_0_compat.con" as lemma.
896
897 (* UNEXPORTED
898 Hint Resolve Rinv_lt_0_compat: real.
899 *)
900
901 (*#********)
902
903 inline procedural "cic:/Coq/Reals/RIneq/Rinv_lt_contravar.con" as lemma.
904
905 inline procedural "cic:/Coq/Reals/RIneq/Rinv_1_lt_contravar.con" as lemma.
906
907 (* UNEXPORTED
908 Hint Resolve Rinv_1_lt_contravar: real.
909 *)
910
911 (*#********************************************************)
912
913 (*#*      Greater                                         *)
914
915 (*#********************************************************)
916
917 (*#*********)
918
919 inline procedural "cic:/Coq/Reals/RIneq/Rge_antisym.con" as lemma.
920
921 (*#*********)
922
923 inline procedural "cic:/Coq/Reals/RIneq/Rnot_lt_ge.con" as lemma.
924
925 (*#*********)
926
927 inline procedural "cic:/Coq/Reals/RIneq/Rnot_lt_le.con" as lemma.
928
929 (*#*********)
930
931 inline procedural "cic:/Coq/Reals/RIneq/Rnot_gt_le.con" as lemma.
932
933 (*#*********)
934
935 inline procedural "cic:/Coq/Reals/RIneq/Rgt_ge.con" as lemma.
936
937 (*#*********)
938
939 inline procedural "cic:/Coq/Reals/RIneq/Rge_gt_trans.con" as lemma.
940
941 (*#*********)
942
943 inline procedural "cic:/Coq/Reals/RIneq/Rgt_ge_trans.con" as lemma.
944
945 (*#*********)
946
947 inline procedural "cic:/Coq/Reals/RIneq/Rgt_trans.con" as lemma.
948
949 (*#*********)
950
951 inline procedural "cic:/Coq/Reals/RIneq/Rge_trans.con" as lemma.
952
953 (*#*********)
954
955 inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_0_plus_1.con" as lemma.
956
957 (* UNEXPORTED
958 Hint Resolve Rle_lt_0_plus_1: real.
959 *)
960
961 (*#*********)
962
963 inline procedural "cic:/Coq/Reals/RIneq/Rlt_plus_1.con" as lemma.
964
965 (* UNEXPORTED
966 Hint Resolve Rlt_plus_1: real.
967 *)
968
969 (*#*********)
970
971 inline procedural "cic:/Coq/Reals/RIneq/tech_Rgt_minus.con" as lemma.
972
973 (*#**********)
974
975 inline procedural "cic:/Coq/Reals/RIneq/Rplus_gt_compat_l.con" as lemma.
976
977 (* UNEXPORTED
978 Hint Resolve Rplus_gt_compat_l: real.
979 *)
980
981 (*#**********)
982
983 inline procedural "cic:/Coq/Reals/RIneq/Rplus_gt_reg_l.con" as lemma.
984
985 (*#**********)
986
987 inline procedural "cic:/Coq/Reals/RIneq/Rplus_ge_compat_l.con" as lemma.
988
989 (* UNEXPORTED
990 Hint Resolve Rplus_ge_compat_l: real.
991 *)
992
993 (*#**********)
994
995 inline procedural "cic:/Coq/Reals/RIneq/Rplus_ge_reg_l.con" as lemma.
996
997 (*#**********)
998
999 inline procedural "cic:/Coq/Reals/RIneq/Rmult_ge_compat_r.con" as lemma.
1000
1001 (*#**********)
1002
1003 inline procedural "cic:/Coq/Reals/RIneq/Rgt_minus.con" as lemma.
1004
1005 (*#********)
1006
1007 inline procedural "cic:/Coq/Reals/RIneq/minus_Rgt.con" as lemma.
1008
1009 (*#*********)
1010
1011 inline procedural "cic:/Coq/Reals/RIneq/Rge_minus.con" as lemma.
1012
1013 (*#********)
1014
1015 inline procedural "cic:/Coq/Reals/RIneq/minus_Rge.con" as lemma.
1016
1017 (*#********)
1018
1019 inline procedural "cic:/Coq/Reals/RIneq/Rmult_gt_0_compat.con" as lemma.
1020
1021 (*#********)
1022
1023 inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_0_compat.con" as lemma.
1024
1025 (*#**********)
1026
1027 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_0_l.con" as lemma.
1028
1029 inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_R0.con" as lemma.
1030
1031 (*#**********)
1032
1033 inline procedural "cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0_l.con" as lemma.
1034
1035 inline procedural "cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0.con" as lemma.
1036
1037 (*#*********************************************************)
1038
1039 (*#*       Injection from [N] to [R]                       *)
1040
1041 (*#*********************************************************)
1042
1043 (*#*********)
1044
1045 inline procedural "cic:/Coq/Reals/RIneq/S_INR.con" as lemma.
1046
1047 (*#*********)
1048
1049 inline procedural "cic:/Coq/Reals/RIneq/S_O_plus_INR.con" as lemma.
1050
1051 (*#*********)
1052
1053 inline procedural "cic:/Coq/Reals/RIneq/plus_INR.con" as lemma.
1054
1055 (*#*********)
1056
1057 inline procedural "cic:/Coq/Reals/RIneq/minus_INR.con" as lemma.
1058
1059 (*#********)
1060
1061 inline procedural "cic:/Coq/Reals/RIneq/mult_INR.con" as lemma.
1062
1063 (* UNEXPORTED
1064 Hint Resolve plus_INR minus_INR mult_INR: real.
1065 *)
1066
1067 (*#********)
1068
1069 inline procedural "cic:/Coq/Reals/RIneq/lt_INR_0.con" as lemma.
1070
1071 (* UNEXPORTED
1072 Hint Resolve lt_INR_0: real.
1073 *)
1074
1075 inline procedural "cic:/Coq/Reals/RIneq/lt_INR.con" as lemma.
1076
1077 (* UNEXPORTED
1078 Hint Resolve lt_INR: real.
1079 *)
1080
1081 inline procedural "cic:/Coq/Reals/RIneq/INR_lt_1.con" as lemma.
1082
1083 (* UNEXPORTED
1084 Hint Resolve INR_lt_1: real.
1085 *)
1086
1087 (*#*********)
1088
1089 inline procedural "cic:/Coq/Reals/RIneq/INR_pos.con" as lemma.
1090
1091 (* UNEXPORTED
1092 Hint Resolve INR_pos: real.
1093 *)
1094
1095 (*#*********)
1096
1097 inline procedural "cic:/Coq/Reals/RIneq/pos_INR.con" as lemma.
1098
1099 (* UNEXPORTED
1100 Hint Resolve pos_INR: real.
1101 *)
1102
1103 inline procedural "cic:/Coq/Reals/RIneq/INR_lt.con" as lemma.
1104
1105 (* UNEXPORTED
1106 Hint Resolve INR_lt: real.
1107 *)
1108
1109 (*#********)
1110
1111 inline procedural "cic:/Coq/Reals/RIneq/le_INR.con" as lemma.
1112
1113 (* UNEXPORTED
1114 Hint Resolve le_INR: real.
1115 *)
1116
1117 (*#*********)
1118
1119 inline procedural "cic:/Coq/Reals/RIneq/not_INR_O.con" as lemma.
1120
1121 (* UNEXPORTED
1122 Hint Immediate not_INR_O: real.
1123 *)
1124
1125 (*#*********)
1126
1127 inline procedural "cic:/Coq/Reals/RIneq/not_O_INR.con" as lemma.
1128
1129 (* UNEXPORTED
1130 Hint Resolve not_O_INR: real.
1131 *)
1132
1133 inline procedural "cic:/Coq/Reals/RIneq/not_nm_INR.con" as lemma.
1134
1135 (* UNEXPORTED
1136 Hint Resolve not_nm_INR: real.
1137 *)
1138
1139 inline procedural "cic:/Coq/Reals/RIneq/INR_eq.con" as lemma.
1140
1141 (* UNEXPORTED
1142 Hint Resolve INR_eq: real.
1143 *)
1144
1145 inline procedural "cic:/Coq/Reals/RIneq/INR_le.con" as lemma.
1146
1147 (* UNEXPORTED
1148 Hint Resolve INR_le: real.
1149 *)
1150
1151 inline procedural "cic:/Coq/Reals/RIneq/not_1_INR.con" as lemma.
1152
1153 (* UNEXPORTED
1154 Hint Resolve not_1_INR: real.
1155 *)
1156
1157 (*#*********************************************************)
1158
1159 (*#*      Injection from [Z] to [R]                        *)
1160
1161 (*#*********************************************************)
1162
1163 (*#*********)
1164
1165 inline procedural "cic:/Coq/Reals/RIneq/IZN.con" as lemma.
1166
1167 (*#*********)
1168
1169 inline procedural "cic:/Coq/Reals/RIneq/INR_IZR_INZ.con" as lemma.
1170
1171 inline procedural "cic:/Coq/Reals/RIneq/plus_IZR_NEG_POS.con" as lemma.
1172
1173 (*#*********)
1174
1175 inline procedural "cic:/Coq/Reals/RIneq/plus_IZR.con" as lemma.
1176
1177 (*#*********)
1178
1179 inline procedural "cic:/Coq/Reals/RIneq/mult_IZR.con" as lemma.
1180
1181 (*#*********)
1182
1183 inline procedural "cic:/Coq/Reals/RIneq/Ropp_Ropp_IZR.con" as lemma.
1184
1185 (*#*********)
1186
1187 inline procedural "cic:/Coq/Reals/RIneq/Z_R_minus.con" as lemma.
1188
1189 (*#*********)
1190
1191 inline procedural "cic:/Coq/Reals/RIneq/lt_O_IZR.con" as lemma.
1192
1193 (*#*********)
1194
1195 inline procedural "cic:/Coq/Reals/RIneq/lt_IZR.con" as lemma.
1196
1197 (*#*********)
1198
1199 inline procedural "cic:/Coq/Reals/RIneq/eq_IZR_R0.con" as lemma.
1200
1201 (*#*********)
1202
1203 inline procedural "cic:/Coq/Reals/RIneq/eq_IZR.con" as lemma.
1204
1205 (*#*********)
1206
1207 inline procedural "cic:/Coq/Reals/RIneq/not_O_IZR.con" as lemma.
1208
1209 (*#********)
1210
1211 inline procedural "cic:/Coq/Reals/RIneq/le_O_IZR.con" as lemma.
1212
1213 (*#*********)
1214
1215 inline procedural "cic:/Coq/Reals/RIneq/le_IZR.con" as lemma.
1216
1217 (*#*********)
1218
1219 inline procedural "cic:/Coq/Reals/RIneq/le_IZR_R1.con" as lemma.
1220
1221 (*#*********)
1222
1223 inline procedural "cic:/Coq/Reals/RIneq/IZR_ge.con" as lemma.
1224
1225 inline procedural "cic:/Coq/Reals/RIneq/IZR_le.con" as lemma.
1226
1227 inline procedural "cic:/Coq/Reals/RIneq/IZR_lt.con" as lemma.
1228
1229 inline procedural "cic:/Coq/Reals/RIneq/one_IZR_lt1.con" as lemma.
1230
1231 inline procedural "cic:/Coq/Reals/RIneq/one_IZR_r_R1.con" as lemma.
1232
1233 (*#*********)
1234
1235 inline procedural "cic:/Coq/Reals/RIneq/single_z_r_R1.con" as lemma.
1236
1237 (*#*********)
1238
1239 inline procedural "cic:/Coq/Reals/RIneq/tech_single_z_r_R1.con" as lemma.
1240
1241 (*#****************************************************************)
1242
1243 (*#* Definitions of new types                                     *)
1244
1245 (*#****************************************************************)
1246
1247 inline procedural "cic:/Coq/Reals/RIneq/nonnegreal.ind".
1248
1249 inline procedural "cic:/Coq/Reals/RIneq/posreal.ind".
1250
1251 inline procedural "cic:/Coq/Reals/RIneq/nonposreal.ind".
1252
1253 inline procedural "cic:/Coq/Reals/RIneq/negreal.ind".
1254
1255 inline procedural "cic:/Coq/Reals/RIneq/nonzeroreal.ind".
1256
1257 (*#*********)
1258
1259 inline procedural "cic:/Coq/Reals/RIneq/prod_neq_R0.con" as lemma.
1260
1261 (*#********)
1262
1263 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_pos.con" as lemma.
1264
1265 inline procedural "cic:/Coq/Reals/RIneq/double.con" as lemma.
1266
1267 inline procedural "cic:/Coq/Reals/RIneq/double_var.con" as lemma.
1268
1269 (*#*********************************************************)
1270
1271 (*#* Other rules about < and <=                            *)
1272
1273 (*#*********************************************************)
1274
1275 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con" as lemma.
1276
1277 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_lt_0_compat.con" as lemma.
1278
1279 inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_le_0_compat.con" as lemma.
1280
1281 inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_le_0_compat.con" as lemma.
1282
1283 inline procedural "cic:/Coq/Reals/RIneq/plus_le_is_le.con" as lemma.
1284
1285 inline procedural "cic:/Coq/Reals/RIneq/plus_lt_is_lt.con" as lemma.
1286
1287 inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_0_lt_compat.con" as lemma.
1288
1289 inline procedural "cic:/Coq/Reals/RIneq/le_epsilon.con" as lemma.
1290
1291 (*#*********)
1292
1293 inline procedural "cic:/Coq/Reals/RIneq/completeness_weak.con" as lemma.
1294