Empty types not in Prop and empty types elimination handled correctly.

[helm.git] / matita / contribs / CoRN-Decl / reals / NRootIR.ma

diff --git a/matita/contribs/CoRN-Decl/reals/NRootIR.ma b/matita/contribs/CoRN-Decl/reals/NRootIR.ma
index 3688480985b751afa3fa2d40a7d5f603099ad361..0f976d765be65e4630453f83dcff9b6a98157cc9 100644 (file)
--- a/matita/contribs/CoRN-Decl/reals/NRootIR.ma
+++ b/matita/contribs/CoRN-Decl/reals/NRootIR.ma
@@ -16,20 +16,20 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/reals/NRootIR".
 
+include "CoRN.ma".
+
 (* $Id: NRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
 
 (*#* printing NRoot %\ensuremath{\sqrt[n]{\cdot}}% *)
 
 (*#* printing sqrt %\ensuremath{\sqrt{\cdot}}% *)
 
-(* INCLUDE
-OddPolyRootIR
-*)
+include "reals/OddPolyRootIR.ma".
 
 (*#* * Roots of Real Numbers *)
 
 (* UNEXPORTED
-Section NRoot.
+Section NRoot
 *)
 
 (*#* ** Existence of roots
@@ -39,24 +39,24 @@ Section NRoot.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/reals/NRootIR/n.var.
+alias id "n" = "cic:/CoRN/reals/NRootIR/NRoot/n.var".
 
-inline cic:/CoRN/reals/NRootIR/n_pos.var.
+alias id "n_pos" = "cic:/CoRN/reals/NRootIR/NRoot/n_pos.var".
 
-inline cic:/CoRN/reals/NRootIR/c.var.
+alias id "c" = "cic:/CoRN/reals/NRootIR/NRoot/c.var".
 
-inline cic:/CoRN/reals/NRootIR/c_nonneg.var.
+alias id "c_nonneg" = "cic:/CoRN/reals/NRootIR/NRoot/c_nonneg.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/reals/NRootIR/p.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot/p.con" "NRoot__".
 
 (* end hide *)
 
-inline cic:/CoRN/reals/NRootIR/CnrootIR.con.
+inline "cic:/CoRN/reals/NRootIR/CnrootIR.con".
 
 (* UNEXPORTED
-End NRoot.
+End NRoot
 *)
 
 (*#* We define the root of order [n] for any nonnegative real number and 
@@ -72,48 +72,48 @@ prove its main properties:
 *)
 
 (* UNEXPORTED
-Section Nth_Root.
+Section Nth_Root
 *)
 
-inline cic:/CoRN/reals/NRootIR/nroot.con.
+inline "cic:/CoRN/reals/NRootIR/nroot.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_power.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_power.con".
 
 (* UNEXPORTED
 Hint Resolve NRoot_power: algebra.
 *)
 
-inline cic:/CoRN/reals/NRootIR/NRoot_nonneg.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_nonneg.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_pos.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_pos.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_power'.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_power'.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_pres_less.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_pres_less.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_less_one.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_less_one.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_cancel.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_cancel.con".
 
 (*#* %\begin{convention}% Let [x,y] be nonnegative real numbers.
 %\end{convention}% *)
 
-inline cic:/CoRN/reals/NRootIR/x.var.
+alias id "x" = "cic:/CoRN/reals/NRootIR/Nth_Root/x.var".
 
-inline cic:/CoRN/reals/NRootIR/y.var.
+alias id "y" = "cic:/CoRN/reals/NRootIR/Nth_Root/y.var".
 
-inline cic:/CoRN/reals/NRootIR/Hx.var.
+alias id "Hx" = "cic:/CoRN/reals/NRootIR/Nth_Root/Hx.var".
 
-inline cic:/CoRN/reals/NRootIR/Hy.var.
+alias id "Hy" = "cic:/CoRN/reals/NRootIR/Nth_Root/Hy.var".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_wd.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_wd.con".
 
-inline cic:/CoRN/reals/NRootIR/NRoot_unique.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_unique.con".
 
 (* UNEXPORTED
-End Nth_Root.
+End Nth_Root
 *)
 
 (* UNEXPORTED
@@ -124,56 +124,56 @@ Implicit Arguments NRoot [x n].
 Hint Resolve NRoot_power NRoot_power': algebra.
 *)
 
-inline cic:/CoRN/reals/NRootIR/NRoot_resp_leEq.con.
+inline "cic:/CoRN/reals/NRootIR/NRoot_resp_leEq.con".
 
 (*#**********************************)
 
 (* UNEXPORTED
-Section Square_root.
+Section Square_root
 *)
 
 (*#**********************************)
 
 (*#* ** Square root *)
 
-inline cic:/CoRN/reals/NRootIR/sqrt.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_sqr.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_sqr.con".
 
 (* UNEXPORTED
 Hint Resolve sqrt_sqr: algebra.
 *)
 
-inline cic:/CoRN/reals/NRootIR/sqrt_nonneg.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_nonneg.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_wd.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_wd.con".
 
 (* UNEXPORTED
 Hint Resolve sqrt_wd: algebra_c.
 *)
 
-inline cic:/CoRN/reals/NRootIR/sqrt_to_nonneg.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_to_nonneg.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_to_nonpos.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_to_nonpos.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_mult.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_mult.con".
 
 (* UNEXPORTED
 Hint Resolve sqrt_mult: algebra.
 *)
 
-inline cic:/CoRN/reals/NRootIR/sqrt_mult_wd.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_mult_wd.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_less.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_less.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_less'.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_less'.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_resp_leEq.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_resp_leEq.con".
 
-inline cic:/CoRN/reals/NRootIR/sqrt_resp_less.con.
+inline "cic:/CoRN/reals/NRootIR/sqrt_resp_less.con".
 
 (* UNEXPORTED
-End Square_root.
+End Square_root
 *)
 
 (* UNEXPORTED
@@ -185,7 +185,7 @@ Hint Resolve sqrt_sqr sqrt_mult: algebra.
 *)
 
 (* UNEXPORTED
-Section Absolute_Props.
+Section Absolute_Props
 *)
 
 (*#* ** More on absolute value
@@ -194,60 +194,60 @@ With the help of square roots, we can prove some more properties of absolute
 values in [IR].
 *)
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_sqrt_sqr.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_sqrt_sqr.con".
 
 (* UNEXPORTED
 Hint Resolve AbsIR_sqrt_sqr: algebra.
 *)
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_resp_mult.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_resp_mult.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_mult_pos.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_mult_pos'.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos'.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_nexp.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_nexp.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_nexp_op.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_nexp_op.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_less_square.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_less_square.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_leEq_square.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_leEq_square.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_division.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_division.con".
 
 (*#* Some special cases. *)
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_recip.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_recip.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_div_two.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_div_two.con".
 
 (*#* Cauchy-Schwartz for IR and variants on that subject. *)
 
-inline cic:/CoRN/reals/NRootIR/triangle_IR.con.
+inline "cic:/CoRN/reals/NRootIR/triangle_IR.con".
 
-inline cic:/CoRN/reals/NRootIR/triangle_SumIR.con.
+inline "cic:/CoRN/reals/NRootIR/triangle_SumIR.con".
 
-inline cic:/CoRN/reals/NRootIR/triangle_IR_minus.con.
+inline "cic:/CoRN/reals/NRootIR/triangle_IR_minus.con".
 
-inline cic:/CoRN/reals/NRootIR/weird_triangleIR.con.
+inline "cic:/CoRN/reals/NRootIR/weird_triangleIR.con".
 
-inline cic:/CoRN/reals/NRootIR/triangle_IR_minus'.con.
+inline "cic:/CoRN/reals/NRootIR/triangle_IR_minus'.con".
 
-inline cic:/CoRN/reals/NRootIR/triangle_SumxIR.con.
+inline "cic:/CoRN/reals/NRootIR/triangle_SumxIR.con".
 
-inline cic:/CoRN/reals/NRootIR/triangle_Sum2IR.con.
+inline "cic:/CoRN/reals/NRootIR/triangle_Sum2IR.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_str_bnd_AbsIR.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_str_bnd_AbsIR.con".
 
-inline cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con.
+inline "cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con".
 
 (* UNEXPORTED
-End Absolute_Props.
+End Absolute_Props
 *)
 
 (* UNEXPORTED
-Section Consequences.
+Section Consequences
 *)
 
 (*#* **Cauchy sequences
@@ -257,13 +257,13 @@ Cauchy sequence that is never zero and whose Limit is not zero is also a
 Cauchy sequence.
 *)
 
-inline cic:/CoRN/reals/NRootIR/Cauchy_Lim_recip.con.
+inline "cic:/CoRN/reals/NRootIR/Cauchy_Lim_recip.con".
 
-inline cic:/CoRN/reals/NRootIR/Cauchy_recip.con.
+inline "cic:/CoRN/reals/NRootIR/Cauchy_recip.con".
 
-inline cic:/CoRN/reals/NRootIR/Lim_recip.con.
+inline "cic:/CoRN/reals/NRootIR/Lim_recip.con".
 
 (* UNEXPORTED
-End Consequences.
+End Consequences
 *)