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 (* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *)
21 include "reals/NRootIR.ma".
23 (*#* printing p3m %\ensuremath{\frac13\hat{\ }}% *)
25 (*#* printing Halfeps %\ensuremath{\frac\varepsilon2}% *)
27 (*#* * Technical lemmas for the FTA
36 %\begin{convention}% Let [a:nat->IR] and [n:nat] such that [0 < n],
37 [forall (k : nat) (Zero [<=] (a k))], [(a n) [=] One] and [a_0 : IR],
38 and [eps : IR] such that [(Zero [<] eps)] and [(eps [<=] a_0)].
43 cic:/CoRN/fta/KeyLemma/Key_Lemma/a.var
47 cic:/CoRN/fta/KeyLemma/Key_Lemma/n.var
51 cic:/CoRN/fta/KeyLemma/Key_Lemma/gt_n_0.var
55 cic:/CoRN/fta/KeyLemma/Key_Lemma/eps.var
59 cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_pos.var
63 cic:/CoRN/fta/KeyLemma/Key_Lemma/a_nonneg.var
67 cic:/CoRN/fta/KeyLemma/Key_Lemma/a_n_1.var
71 cic:/CoRN/fta/KeyLemma/Key_Lemma/a_0.var
75 cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_le_a_0.var
78 inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_nonneg.con" as lemma.
80 inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_fuzz.con" as lemma.
82 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1a.con" as lemma.
84 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1b.con" as lemma.
86 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1c.con" as lemma.
88 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1.con" as lemma.
90 inline procedural "cic:/CoRN/fta/KeyLemma/p3m.con" as definition.
92 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pos.con" as lemma.
94 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_S.con" as lemma.
97 Hint Resolve p3m_S: algebra.
100 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_P.con" as lemma.
102 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_aux.con" as lemma.
104 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pow.con" as lemma.
107 Hint Resolve p3m_aux: algebra.
110 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_0.con" as lemma.
113 Hint Resolve p3m_0: algebra.
116 inline procedural "cic:/CoRN/fta/KeyLemma/third_pos.con" as lemma.
119 Hint Resolve third_pos: algebra.
122 inline procedural "cic:/CoRN/fta/KeyLemma/third_less_one.con" as lemma.
125 Hint Resolve third_less_one: algebra.
128 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon.con" as lemma.
130 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon'.con" as lemma.
132 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_small.con" as lemma.
134 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_smaller.con" as lemma.
136 inline procedural "cic:/CoRN/fta/KeyLemma/chfun.con" as definition.
138 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_1.con" as lemma.
140 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_2.con" as lemma.
142 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_3.con" as lemma.
144 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_4.con" as lemma.
146 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps.con" as definition.
148 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_pos.con" as lemma.
150 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_Halfeps.con" as lemma.
153 Hint Resolve Halfeps_Halfeps: algebra.
156 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_eps.con" as lemma.
158 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_trans.con" as lemma.
160 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1a.con" as lemma.
163 Hint Resolve Key_1a: algebra.
166 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1b.con" as lemma.
168 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1.con" as lemma.
170 inline procedural "cic:/CoRN/fta/KeyLemma/Key_2.con" as lemma.
172 inline procedural "cic:/CoRN/fta/KeyLemma/Key.con" as lemma.
181 Hint Resolve p3m_S p3m_P p3m_pow: algebra.