...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / complex / NRootCC.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/complex/NRootCC.mma b/helm/software/matita/contribs/CoRN-Procedural/complex/NRootCC.mma
index 57f1f1a917f99720cdf544c7ed92c08d3c14c67d..1fa6e5cfe02dce388b49ff5e4ce8af321a397f71 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/complex/NRootCC.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/complex/NRootCC.mma
@@ -37,9 +37,9 @@ Properties of non-zero complex numbers
 Section CC_ap_zero
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/cc_ap_zero.con".
+inline procedural "cic:/CoRN/complex/NRootCC/cc_ap_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con".
+inline procedural "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con" as lemma.
 
 (* UNEXPORTED
 End CC_ap_zero
@@ -51,7 +51,7 @@ End CC_ap_zero
 Section Imag_to_Real
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/imag_to_real.con".
+inline procedural "cic:/CoRN/complex/NRootCC/imag_to_real.con" as lemma.
 
 (* UNEXPORTED
 End Imag_to_Real
@@ -63,25 +63,25 @@ End Imag_to_Real
 Section NRootI
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/sqrt_Half.con".
+inline procedural "cic:/CoRN/complex/NRootCC/sqrt_Half.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I.con".
+inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con".
+inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nroot_I.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nroot_I.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nroot_I_nexp: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con" as lemma.
 
 (* UNEXPORTED
 End NRootI
@@ -107,77 +107,83 @@ Define [c2 := a[^]2[+]b[^]2], [c := sqrt c2], [a'2 := (c[+]a) [*]Half],
 %\end{convention}%
 *)
 
-alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a.var
+*)
 
-alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b.var
+*)
 
-alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b_.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c2.con" "NRootCC_1__NRootCC_1_ap_real__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c2.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con" as lemma.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c.con" "NRootCC_1__NRootCC_1_ap_real__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'2.con" "NRootCC_1__NRootCC_1_ap_real__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'2.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con" as lemma.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'.con" "NRootCC_1__NRootCC_1_ap_real__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'2.con" "NRootCC_1__NRootCC_1_ap_real__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'2.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con" as lemma.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'.con" "NRootCC_1__NRootCC_1_ap_real__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a3.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a3.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a4.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a4.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nrCC1_a4: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a5.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a5.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6'.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6'.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nrCC1_a5: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nrCC1_a3 nrCC1_a7_upper nrCC1_a7_lower: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_1_ap_real
@@ -196,19 +202,25 @@ Section NRootCC_1_ap_imag
 %\end{convention}%
 *)
 
-alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a.var
+*)
 
-alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b.var
+*)
 
-alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a_.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/c'.con" "NRootCC_1__NRootCC_1_ap_imag__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/c'.con" "NRootCC_1__NRootCC_1_ap_imag__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a'.con" "NRootCC_1__NRootCC_1_ap_imag__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a'.con" "NRootCC_1__NRootCC_1_ap_imag__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b'.con" "NRootCC_1__NRootCC_1_ap_imag__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b'.con" "NRootCC_1__NRootCC_1_ap_imag__" as definition.
 
 (* end hide *)
 
@@ -216,7 +228,7 @@ inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b'.con"
 Hint Resolve sqrt_I_nexp: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_1_ap_imag
@@ -224,7 +236,7 @@ End NRootCC_1_ap_imag
 
 (*#* We now define the roots of arbitrary non zero complex numbers. *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_1
@@ -239,17 +251,25 @@ Section NRootCC_2
 %\end{convention}%
 *)
 
-alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_2/n.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_2/n.var
+*)
 
-alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_2/c.var
+*)
 
-alias id "z" = "cic:/CoRN/complex/NRootCC/NRootCC_2/z.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_2/z.var
+*)
 
-alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_2/c_.var
+*)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2'.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2'.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_2
@@ -259,44 +279,52 @@ End NRootCC_2
 Section NRootCC_3
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/Im_poly.con".
+inline procedural "cic:/CoRN/complex/NRootCC/Im_poly.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a1.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a1.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a2.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a2.con" as lemma.
 
 (*#*
 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)] and [n : nat].
 %\end{convention}%
 *)
 
-alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_3/a.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_3/a.var
+*)
 
-alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_3/b.var
+*)
 
-alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_3/b_.var
+*)
 
-alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3/n.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_3/n.var
+*)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a3.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a3.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a4.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a4.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a5.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a5.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a6.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a6.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly'.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly'.con" as definition.
 
 (* UNEXPORTED
 Hint Resolve nrCC3_a3: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a7.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a7.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a8.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a8.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nth_coeff_p_mult_c_: algebra.
@@ -306,15 +334,15 @@ Hint Resolve nth_coeff_p_mult_c_: algebra.
 Hint Resolve nrCC3_a6: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a9.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a9.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con" as definition.
 
 (* UNEXPORTED
 Hint Resolve nrCC3_a1 nrCC3_a7: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nrootCC_3_: algebra.
@@ -324,7 +352,7 @@ Hint Resolve nrootCC_3_: algebra.
 Hint Resolve calculate_Im: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nrCC3_a2: algebra.
@@ -334,7 +362,7 @@ Hint Resolve nrCC3_a2: algebra.
 Hint Resolve nrCC3_a9: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_3
@@ -349,17 +377,23 @@ Section NRootCC_3'
 %\end{convention}%
 *)
 
-alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/c.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_3'/c.var
+*)
 
-alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_3'/n.var
+*)
 
-alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_3'/n_.var
+*)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_3'
@@ -379,19 +413,29 @@ Section NRootCC_4_ap_real
 %\end{convention}%
 *)
 
-alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/a.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/a.var
+*)
 
-alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b.var
+*)
 
-alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b_.var
+*)
 
-alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n.var
+*)
 
-alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n_.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/c.con" "NRootCC_4__NRootCC_4_ap_real__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/c.con" "NRootCC_4__NRootCC_4_ap_real__" as definition.
 
 (* end hide *)
 
@@ -403,24 +447,30 @@ Section NRootCC_4_solutions
 Hint Resolve nrootCC_3: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1.con" as lemma.
 
 (*#*
 %\begin{convention}% Let [r2',c2 : IR] and [r2'_ : (r2' [#] Zero)].
 %\end{convention}%
 *)
 
-alias id "r2'" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'.var
+*)
 
-alias id "c2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/c2.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/c2.var
+*)
 
-alias id "r2'_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'_.var
+*)
 
 (* UNEXPORTED
 Hint Resolve nrootCC_3': algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_4_solutions
@@ -437,53 +487,61 @@ and [(y2[*] (r[^] (2) [+]One)) [^]n [=] a[^] (2) [+]b[^] (2)].
 %\end{convention}%
 *)
 
-alias id "r" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r.var
+*)
 
-alias id "r_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r_property.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r_property.var
+*)
 
-alias id "y2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2.var
+*)
 
-alias id "y2_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2_property.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2_property.var
+*)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a2.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a2.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a3.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a3.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a4.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a4.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_y.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_y.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_x.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_x.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/x.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/x.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a5.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a5.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a6.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a6.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_z.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_z.con" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/z.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/z.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a7.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a7.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nrCC4_a6: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a8.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a8.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a9.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a9.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_4_equations
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a10.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a10.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_4_ap_real
@@ -499,39 +557,49 @@ and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b'].
 %\end{convention}%
 *)
 
-alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a.var
+*)
 
-alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b.var
+*)
 
-alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a_.var
+*)
 
-alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n.var
+*)
 
-alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n_.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/c'.con" "NRootCC_4__NRootCC_4_ap_imag__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/c'.con" "NRootCC_4__NRootCC_4_ap_imag__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a'.con" "NRootCC_4__NRootCC_4_ap_imag__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a'.con" "NRootCC_4__NRootCC_4_ap_imag__" as definition.
 
-inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b'.con" "NRootCC_4__NRootCC_4_ap_imag__".
+inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b'.con" "NRootCC_4__NRootCC_4_ap_imag__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nroot_minus_I_nexp: algebra.
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_4_ap_imag
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_4
@@ -543,9 +611,9 @@ End NRootCC_4
 Section NRootCC_5
 *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a2.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a2.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a3.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a3.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve nrCC_5a3: algebra.
@@ -556,13 +624,17 @@ Hint Resolve nrCC_5a3: algebra.
 %\end{convention}%
 *)
 
-alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_5/c.var
+*)
 
-alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c_.var".
+(* UNEXPORTED
+cic:/CoRN/complex/NRootCC/NRootCC_5/c_.var
+*)
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a4.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a4.con" as lemma.
 
-inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_5.con".
+inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_5.con" as lemma.
 
 (* UNEXPORTED
 End NRootCC_5
@@ -570,5 +642,5 @@ End NRootCC_5
 
 (*#* Final definition *)
 
-inline procedural "cic:/CoRN/complex/NRootCC/CnrootCC.con".
+inline procedural "cic:/CoRN/complex/NRootCC/CnrootCC.con" as definition.