(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "CoRN.ma".

(* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *)

include "reals/NRootIR.ma".

(*#* printing p3m %\ensuremath{\frac13\hat{\ }}% *)

(*#* printing Halfeps %\ensuremath{\frac\varepsilon2}% *)

(*#* * Technical lemmas for the FTA
** Key Lemma
*)

(* UNEXPORTED
Section Key_Lemma
*)

(*#*
%\begin{convention}% Let [a:nat->IR] and [n:nat] such that [0 < n],
[forall (k : nat) (Zero [<=] (a k))], [(a n) [=] One] and [a_0 : IR],
and [eps : IR] such that [(Zero [<] eps)] and [(eps [<=] a_0)].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/a.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/n.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/gt_n_0.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/eps.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_pos.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/a_nonneg.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/a_n_1.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/a_0.var
*)

(* UNEXPORTED
cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_le_a_0.var
*)

inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_nonneg.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_fuzz.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/lem_1a.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/lem_1b.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/lem_1c.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/lem_1.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m.con" as definition.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pos.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_S.con" as lemma.

(* UNEXPORTED
Hint Resolve p3m_S: algebra.
*)

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_P.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_aux.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pow.con" as lemma.

(* UNEXPORTED
Hint Resolve p3m_aux: algebra.
*)

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_0.con" as lemma.

(* UNEXPORTED
Hint Resolve p3m_0: algebra.
*)

inline procedural "cic:/CoRN/fta/KeyLemma/third_pos.con" as lemma.

(* UNEXPORTED
Hint Resolve third_pos: algebra.
*)

inline procedural "cic:/CoRN/fta/KeyLemma/third_less_one.con" as lemma.

(* UNEXPORTED
Hint Resolve third_less_one: algebra.
*)

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon'.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_small.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/p3m_smaller.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/chfun.con" as definition.

inline procedural "cic:/CoRN/fta/KeyLemma/chfun_1.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/chfun_2.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/chfun_3.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/chfun_4.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps.con" as definition.

inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_pos.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_Halfeps.con" as lemma.

(* UNEXPORTED
Hint Resolve Halfeps_Halfeps: algebra.
*)

inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_eps.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_trans.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/Key_1a.con" as lemma.

(* UNEXPORTED
Hint Resolve Key_1a: algebra.
*)

inline procedural "cic:/CoRN/fta/KeyLemma/Key_1b.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/Key_1.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/Key_2.con" as lemma.

inline procedural "cic:/CoRN/fta/KeyLemma/Key.con" as lemma.

(* end hide *)

(* UNEXPORTED
End Key_Lemma
*)

(* UNEXPORTED
Hint Resolve p3m_S p3m_P p3m_pow: algebra.
*)