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