some theorems have been moved to more appropriate files in library.

[helm.git] / matita / contribs / CoRN-Decl / fta / FTAreg.ma

diff --git a/matita/contribs/CoRN-Decl/fta/FTAreg.ma b/matita/contribs/CoRN-Decl/fta/FTAreg.ma
index fed20062f61baad9de44701101c9695ca9d4debf..c4522f456059270bacc6b9bc460cc5e902e383f6 100644 (file)
--- a/matita/contribs/CoRN-Decl/fta/FTAreg.ma
+++ b/matita/contribs/CoRN-Decl/fta/FTAreg.ma
@@ -16,19 +16,15 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/fta/FTAreg".
 
+include "CoRN.ma".
+
 (* $Id: FTAreg.v,v 1.4 2004/04/23 10:00:57 lcf Exp $ *)
 
-(* INCLUDE
-KneserLemma
-*)
+include "fta/KneserLemma.ma".
 
-(* INCLUDE
-CPoly_Shift
-*)
+include "fta/CPoly_Shift.ma".
 
-(* INCLUDE
-CPoly_Contin1
-*)
+include "fta/CPoly_Contin1.ma".
 
 (*#* * FTA for regular polynomials
 ** The Kneser sequence
@@ -37,12 +33,12 @@ CPoly_Contin1
 *)
 
 (* UNEXPORTED
-Section Seq_Exists.
+Section Seq_Exists
 *)
 
-inline cic:/CoRN/fta/FTAreg/n.var.
+alias id "n" = "cic:/CoRN/fta/FTAreg/Seq_Exists/n.var".
 
-inline cic:/CoRN/fta/FTAreg/lt0n.var.
+alias id "lt0n" = "cic:/CoRN/fta/FTAreg/Seq_Exists/lt0n.var".
 
 (*#*
 %\begin{convention}% Let [qK] be a real between 0 and 1, with
@@ -56,119 +52,123 @@ Let [p] be a monic polynomial over the complex numbers with degree
 *)
 
 (* UNEXPORTED
-Section Kneser_Sequence.
+Section Kneser_Sequence
 *)
 
-inline cic:/CoRN/fta/FTAreg/qK.var.
+alias id "qK" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qK.var".
+
+alias id "zltq" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/zltq.var".
+
+alias id "qlt1" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qlt1.var".
 
-inline cic:/CoRN/fta/FTAreg/zltq.var.
+alias id "q_prop" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/q_prop.var".
 
-inline cic:/CoRN/fta/FTAreg/qlt1.var.
+alias id "p" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p.var".
 
-inline cic:/CoRN/fta/FTAreg/q_prop.var.
+alias id "mp" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/mp.var".
 
-inline cic:/CoRN/fta/FTAreg/p.var.
+alias id "c0" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/c0.var".
 
-inline cic:/CoRN/fta/FTAreg/mp.var.
+alias id "p0ltc0" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p0ltc0.var".
 
-inline cic:/CoRN/fta/FTAreg/c0.var.
+inline "cic:/CoRN/fta/FTAreg/Knes_tup.ind".
 
-inline cic:/CoRN/fta/FTAreg/p0ltc0.var.
+coercion cic:/matita/CoRN-Decl/fta/FTAreg/z_el.con 0 (* compounds *).
 
-inline cic:/CoRN/fta/FTAreg/Knes_tup.ind.
+inline "cic:/CoRN/fta/FTAreg/Knes_tupp.ind".
 
-inline cic:/CoRN/fta/FTAreg/Knes_tupp.ind.
+coercion cic:/matita/CoRN-Decl/fta/FTAreg/Kntup.con 0 (* compounds *).
 
-inline cic:/CoRN/fta/FTAreg/Knes_fun.con.
+inline "cic:/CoRN/fta/FTAreg/Knes_fun.con".
 
-inline cic:/CoRN/fta/FTAreg/Knes_fun_it.con.
+inline "cic:/CoRN/fta/FTAreg/Knes_fun_it.con".
 
-inline cic:/CoRN/fta/FTAreg/sK.con.
+inline "cic:/CoRN/fta/FTAreg/sK.con".
 
-inline cic:/CoRN/fta/FTAreg/sK_c.con.
+inline "cic:/CoRN/fta/FTAreg/sK_c.con".
 
-inline cic:/CoRN/fta/FTAreg/sK_c0.con.
+inline "cic:/CoRN/fta/FTAreg/sK_c0.con".
 
-inline cic:/CoRN/fta/FTAreg/sK_prop1.con.
+inline "cic:/CoRN/fta/FTAreg/sK_prop1.con".
 
-inline cic:/CoRN/fta/FTAreg/sK_it.con.
+inline "cic:/CoRN/fta/FTAreg/sK_it.con".
 
-inline cic:/CoRN/fta/FTAreg/sK_prop2.con.
+inline "cic:/CoRN/fta/FTAreg/sK_prop2.con".
 
 (* UNEXPORTED
-End Kneser_Sequence.
+End Kneser_Sequence
 *)
 
 (* UNEXPORTED
-Section Seq_Exists_Main.
+Section Seq_Exists_Main
 *)
 
 (*#* **Main results
 *)
 
-inline cic:/CoRN/fta/FTAreg/seq_exists.con.
+inline "cic:/CoRN/fta/FTAreg/seq_exists.con".
 
 (* UNEXPORTED
-End Seq_Exists_Main.
+End Seq_Exists_Main
 *)
 
 (* UNEXPORTED
-End Seq_Exists.
+End Seq_Exists
 *)
 
 (* UNEXPORTED
-Section N_Exists.
+Section N_Exists
 *)
 
-inline cic:/CoRN/fta/FTAreg/n.var.
+alias id "n" = "cic:/CoRN/fta/FTAreg/N_Exists/n.var".
 
-inline cic:/CoRN/fta/FTAreg/lt0n.var.
+alias id "lt0n" = "cic:/CoRN/fta/FTAreg/N_Exists/lt0n.var".
 
-inline cic:/CoRN/fta/FTAreg/q.var.
+alias id "q" = "cic:/CoRN/fta/FTAreg/N_Exists/q.var".
 
-inline cic:/CoRN/fta/FTAreg/zleq.var.
+alias id "zleq" = "cic:/CoRN/fta/FTAreg/N_Exists/zleq.var".
 
-inline cic:/CoRN/fta/FTAreg/qlt1.var.
+alias id "qlt1" = "cic:/CoRN/fta/FTAreg/N_Exists/qlt1.var".
 
-inline cic:/CoRN/fta/FTAreg/c.var.
+alias id "c" = "cic:/CoRN/fta/FTAreg/N_Exists/c.var".
 
-inline cic:/CoRN/fta/FTAreg/zltc.var.
+alias id "zltc" = "cic:/CoRN/fta/FTAreg/N_Exists/zltc.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/fta/FTAreg/q_.con.
+inline "cic:/CoRN/fta/FTAreg/N_Exists/q_.con" "N_Exists__".
 
 (* end hide *)
 
-inline cic:/CoRN/fta/FTAreg/e.var.
+alias id "e" = "cic:/CoRN/fta/FTAreg/N_Exists/e.var".
 
-inline cic:/CoRN/fta/FTAreg/zlte.var.
+alias id "zlte" = "cic:/CoRN/fta/FTAreg/N_Exists/zlte.var".
 
-inline cic:/CoRN/fta/FTAreg/N_exists.con.
+inline "cic:/CoRN/fta/FTAreg/N_exists.con".
 
 (* UNEXPORTED
-End N_Exists.
+End N_Exists
 *)
 
 (* UNEXPORTED
-Section Seq_is_CC_CAuchy.
+Section Seq_is_CC_CAuchy
 *)
 
 (*#* ** The Kneser sequence is Cauchy in [CC] *)
 
-inline cic:/CoRN/fta/FTAreg/n.var.
+alias id "n" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/n.var".
 
-inline cic:/CoRN/fta/FTAreg/lt0n.var.
+alias id "lt0n" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/lt0n.var".
 
-inline cic:/CoRN/fta/FTAreg/q.var.
+alias id "q" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q.var".
 
-inline cic:/CoRN/fta/FTAreg/zleq.var.
+alias id "zleq" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zleq.var".
 
-inline cic:/CoRN/fta/FTAreg/qlt1.var.
+alias id "qlt1" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/qlt1.var".
 
-inline cic:/CoRN/fta/FTAreg/c.var.
+alias id "c" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/c.var".
 
-inline cic:/CoRN/fta/FTAreg/zltc.var.
+alias id "zltc" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zltc.var".
 
 (*#* %\begin{convention}% Let:
  - [q_] prove [q[-]One [#] Zero]
@@ -181,39 +181,39 @@ inline cic:/CoRN/fta/FTAreg/zltc.var.
 
 (* begin hide *)
 
-inline cic:/CoRN/fta/FTAreg/q_.con.
+inline "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q_.con" "Seq_is_CC_CAuchy__".
 
-inline cic:/CoRN/fta/FTAreg/nrtq.con.
+inline "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq.con" "Seq_is_CC_CAuchy__".
 
-inline cic:/CoRN/fta/FTAreg/nrtc.con.
+inline "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtc.con" "Seq_is_CC_CAuchy__".
 
-inline cic:/CoRN/fta/FTAreg/nrtqlt1.con.
+inline "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtqlt1.con" "Seq_is_CC_CAuchy__".
 
-inline cic:/CoRN/fta/FTAreg/nrtq_.con.
+inline "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq_.con" "Seq_is_CC_CAuchy__".
 
 (* end hide *)
 
-inline cic:/CoRN/fta/FTAreg/zlt_nrtq.con.
+inline "cic:/CoRN/fta/FTAreg/zlt_nrtq.con".
 
-inline cic:/CoRN/fta/FTAreg/zlt_nrtc.con.
+inline "cic:/CoRN/fta/FTAreg/zlt_nrtc.con".
 
-inline cic:/CoRN/fta/FTAreg/nrt_pow.con.
+inline "cic:/CoRN/fta/FTAreg/nrt_pow.con".
 
-inline cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con.
+inline "cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con".
 
-inline cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con.
+inline "cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con".
 
-inline cic:/CoRN/fta/FTAreg/SublemmaRe.con.
+inline "cic:/CoRN/fta/FTAreg/SublemmaRe.con".
 
-inline cic:/CoRN/fta/FTAreg/SublemmaIm.con.
+inline "cic:/CoRN/fta/FTAreg/SublemmaIm.con".
 
-inline cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con.
+inline "cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con".
 
 (* UNEXPORTED
-End Seq_is_CC_CAuchy.
+End Seq_is_CC_CAuchy
 *)
 
-inline cic:/CoRN/fta/FTAreg/FTA_monic.con.
+inline "cic:/CoRN/fta/FTAreg/FTA_monic.con".
 
-inline cic:/CoRN/fta/FTAreg/FTA_reg.con.
+inline "cic:/CoRN/fta/FTAreg/FTA_reg.con".