matita/contribs/CoRN-Decl/fta/KeyLemma.ma

   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 set "baseuri" "cic:/matita/CoRN-Decl/fta/KeyLemma".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *)
  22
  23 include "reals/NRootIR.ma".
  24
  25 (*#* printing p3m %\ensuremath{\frac13\hat{\ }}% *)
  26
  27 (*#* printing Halfeps %\ensuremath{\frac\varepsilon2}% *)
  28
  29 (*#* * Technical lemmas for the FTA
  30 ** Key Lemma
  31 *)
  32
  33 (* UNEXPORTED
  34 Section Key_Lemma
  35 *)
  36
  37 (*#*
  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)].
  41 %\end{convention}%
  42 *)
  43
  44 alias id "a" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a.var".
  45
  46 alias id "n" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/n.var".
  47
  48 alias id "gt_n_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/gt_n_0.var".
  49
  50 alias id "eps" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps.var".
  51
  52 alias id "eps_pos" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_pos.var".
  53
  54 alias id "a_nonneg" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_nonneg.var".
  55
  56 alias id "a_n_1" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_n_1.var".
  57
  58 alias id "a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_0.var".
  59
  60 alias id "eps_le_a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_le_a_0.var".
  61
  62 inline "cic:/CoRN/fta/KeyLemma/a_0_eps_nonneg.con".
  63
  64 inline "cic:/CoRN/fta/KeyLemma/a_0_eps_fuzz.con".
  65
  66 inline "cic:/CoRN/fta/KeyLemma/lem_1a.con".
  67
  68 inline "cic:/CoRN/fta/KeyLemma/lem_1b.con".
  69
  70 inline "cic:/CoRN/fta/KeyLemma/lem_1c.con".
  71
  72 inline "cic:/CoRN/fta/KeyLemma/lem_1.con".
  73
  74 inline "cic:/CoRN/fta/KeyLemma/p3m.con".
  75
  76 inline "cic:/CoRN/fta/KeyLemma/p3m_pos.con".
  77
  78 inline "cic:/CoRN/fta/KeyLemma/p3m_S.con".
  79
  80 (* UNEXPORTED
  81 Hint Resolve p3m_S: algebra.
  82 *)
  83
  84 inline "cic:/CoRN/fta/KeyLemma/p3m_P.con".
  85
  86 inline "cic:/CoRN/fta/KeyLemma/p3m_aux.con".
  87
  88 inline "cic:/CoRN/fta/KeyLemma/p3m_pow.con".
  89
  90 (* UNEXPORTED
  91 Hint Resolve p3m_aux: algebra.
  92 *)
  93
  94 inline "cic:/CoRN/fta/KeyLemma/p3m_0.con".
  95
  96 (* UNEXPORTED
  97 Hint Resolve p3m_0: algebra.
  98 *)
  99
 100 inline "cic:/CoRN/fta/KeyLemma/third_pos.con".
 101
 102 (* UNEXPORTED
 103 Hint Resolve third_pos: algebra.
 104 *)
 105
 106 inline "cic:/CoRN/fta/KeyLemma/third_less_one.con".
 107
 108 (* UNEXPORTED
 109 Hint Resolve third_less_one: algebra.
 110 *)
 111
 112 inline "cic:/CoRN/fta/KeyLemma/p3m_mon.con".
 113
 114 inline "cic:/CoRN/fta/KeyLemma/p3m_mon'.con".
 115
 116 inline "cic:/CoRN/fta/KeyLemma/p3m_small.con".
 117
 118 inline "cic:/CoRN/fta/KeyLemma/p3m_smaller.con".
 119
 120 inline "cic:/CoRN/fta/KeyLemma/chfun.con".
 121
 122 inline "cic:/CoRN/fta/KeyLemma/chfun_1.con".
 123
 124 inline "cic:/CoRN/fta/KeyLemma/chfun_2.con".
 125
 126 inline "cic:/CoRN/fta/KeyLemma/chfun_3.con".
 127
 128 inline "cic:/CoRN/fta/KeyLemma/chfun_4.con".
 129
 130 inline "cic:/CoRN/fta/KeyLemma/Halfeps.con".
 131
 132 inline "cic:/CoRN/fta/KeyLemma/Halfeps_pos.con".
 133
 134 inline "cic:/CoRN/fta/KeyLemma/Halfeps_Halfeps.con".
 135
 136 (* UNEXPORTED
 137 Hint Resolve Halfeps_Halfeps: algebra.
 138 *)
 139
 140 inline "cic:/CoRN/fta/KeyLemma/Halfeps_eps.con".
 141
 142 inline "cic:/CoRN/fta/KeyLemma/Halfeps_trans.con".
 143
 144 inline "cic:/CoRN/fta/KeyLemma/Key_1a.con".
 145
 146 (* UNEXPORTED
 147 Hint Resolve Key_1a: algebra.
 148 *)
 149
 150 inline "cic:/CoRN/fta/KeyLemma/Key_1b.con".
 151
 152 inline "cic:/CoRN/fta/KeyLemma/Key_1.con".
 153
 154 inline "cic:/CoRN/fta/KeyLemma/Key_2.con".
 155
 156 inline "cic:/CoRN/fta/KeyLemma/Key.con".
 157
 158 (* end hide *)
 159
 160 (* UNEXPORTED
 161 End Key_Lemma
 162 *)
 163
 164 (* UNEXPORTED
 165 Hint Resolve p3m_S p3m_P p3m_pow: algebra.
 166 *)
 167