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/fta/KeyLemma".
21 (* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *)
23 include "reals/NRootIR.ma".
25 (*#* printing p3m %\ensuremath{\frac13\hat{\ }}% *)
27 (*#* printing Halfeps %\ensuremath{\frac\varepsilon2}% *)
29 (*#* * Technical lemmas for the FTA
38 %\begin{convention}% Let [a:nat->IR] and [n:nat] such that [0 < n],
39 [forall (k : nat) (Zero [<=] (a k))], [(a n) [=] One] and [a_0 : IR],
40 and [eps : IR] such that [(Zero [<] eps)] and [(eps [<=] a_0)].
44 alias id "a" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a.var".
46 alias id "n" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/n.var".
48 alias id "gt_n_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/gt_n_0.var".
50 alias id "eps" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps.var".
52 alias id "eps_pos" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_pos.var".
54 alias id "a_nonneg" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_nonneg.var".
56 alias id "a_n_1" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_n_1.var".
58 alias id "a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_0.var".
60 alias id "eps_le_a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_le_a_0.var".
62 inline "cic:/CoRN/fta/KeyLemma/a_0_eps_nonneg.con".
64 inline "cic:/CoRN/fta/KeyLemma/a_0_eps_fuzz.con".
66 inline "cic:/CoRN/fta/KeyLemma/lem_1a.con".
68 inline "cic:/CoRN/fta/KeyLemma/lem_1b.con".
70 inline "cic:/CoRN/fta/KeyLemma/lem_1c.con".
72 inline "cic:/CoRN/fta/KeyLemma/lem_1.con".
74 inline "cic:/CoRN/fta/KeyLemma/p3m.con".
76 inline "cic:/CoRN/fta/KeyLemma/p3m_pos.con".
78 inline "cic:/CoRN/fta/KeyLemma/p3m_S.con".
81 Hint Resolve p3m_S: algebra.
84 inline "cic:/CoRN/fta/KeyLemma/p3m_P.con".
86 inline "cic:/CoRN/fta/KeyLemma/p3m_aux.con".
88 inline "cic:/CoRN/fta/KeyLemma/p3m_pow.con".
91 Hint Resolve p3m_aux: algebra.
94 inline "cic:/CoRN/fta/KeyLemma/p3m_0.con".
97 Hint Resolve p3m_0: algebra.
100 inline "cic:/CoRN/fta/KeyLemma/third_pos.con".
103 Hint Resolve third_pos: algebra.
106 inline "cic:/CoRN/fta/KeyLemma/third_less_one.con".
109 Hint Resolve third_less_one: algebra.
112 inline "cic:/CoRN/fta/KeyLemma/p3m_mon.con".
114 inline "cic:/CoRN/fta/KeyLemma/p3m_mon'.con".
116 inline "cic:/CoRN/fta/KeyLemma/p3m_small.con".
118 inline "cic:/CoRN/fta/KeyLemma/p3m_smaller.con".
120 inline "cic:/CoRN/fta/KeyLemma/chfun.con".
122 inline "cic:/CoRN/fta/KeyLemma/chfun_1.con".
124 inline "cic:/CoRN/fta/KeyLemma/chfun_2.con".
126 inline "cic:/CoRN/fta/KeyLemma/chfun_3.con".
128 inline "cic:/CoRN/fta/KeyLemma/chfun_4.con".
130 inline "cic:/CoRN/fta/KeyLemma/Halfeps.con".
132 inline "cic:/CoRN/fta/KeyLemma/Halfeps_pos.con".
134 inline "cic:/CoRN/fta/KeyLemma/Halfeps_Halfeps.con".
137 Hint Resolve Halfeps_Halfeps: algebra.
140 inline "cic:/CoRN/fta/KeyLemma/Halfeps_eps.con".
142 inline "cic:/CoRN/fta/KeyLemma/Halfeps_trans.con".
144 inline "cic:/CoRN/fta/KeyLemma/Key_1a.con".
147 Hint Resolve Key_1a: algebra.
150 inline "cic:/CoRN/fta/KeyLemma/Key_1b.con".
152 inline "cic:/CoRN/fta/KeyLemma/Key_1.con".
154 inline "cic:/CoRN/fta/KeyLemma/Key_2.con".
156 inline "cic:/CoRN/fta/KeyLemma/Key.con".
165 Hint Resolve p3m_S p3m_P p3m_pow: algebra.