*)
(* UNEXPORTED
-Section NthCoeff_def.
+Section NthCoeff_def
*)
-inline "cic:/CoRN/algebra/CPoly_NthCoeff/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPoly_NthCoeff/NthCoeff_def/R.var".
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
(*#*
inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_S.con".
(* UNEXPORTED
-End NthCoeff_def.
+End NthCoeff_def
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section NthCoeff_props.
+Section NthCoeff_props
*)
(*#* ** Properties of [nth_coeff] *)
-inline "cic:/CoRN/algebra/CPoly_NthCoeff/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPoly_NthCoeff/NthCoeff_props/R.var".
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_zero.con".
inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_mult.con".
(* UNEXPORTED
-End NthCoeff_props.
+End NthCoeff_props
*)
(* UNEXPORTED