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
%\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
*)
(* 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
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
*)
(* UNEXPORTED
-Section Absolute_Props.
+Section Absolute_Props
*)
(*#* ** More on absolute value
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
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
*)