Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / algebra / CPolynomials.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/algebra/CPolynomials.mma b/helm/software/matita/contribs/CoRN-Procedural/algebra/CPolynomials.mma
index 25155ca721f93839ce7cf83cd55c0e2433b24ed2..99b2465aad99ba938942d074f06a985b972ca002 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/algebra/CPolynomials.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/algebra/CPolynomials.mma
@@ -60,52 +60,52 @@ The intuition behind the type [cpoly] is the following
 
 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly.ind".
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one.con" as definition.
 
 (*#*
 Some useful induction lemmas for doubly quantified propositions.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0'.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0'.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0'.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0'.con" as lemma.
 
 (*#* *** The polynomials form a setoid
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_zero.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_p_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_p_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_p_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_p_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/irreflexive_cpoly_ap.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/irreflexive_cpoly_ap.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/symmetric_cpoly_ap.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/symmetric_cpoly_ap.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cotransitive_cpoly_ap.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cotransitive_cpoly_ap.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/tight_apart_cpoly_ap.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/tight_apart_cpoly_ap.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CSetoid.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CSetoid.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid.con" as definition.
 
 (*#*
 Now that we know that the polynomials form a setoid, we can use the
@@ -117,203 +117,203 @@ the most basic properties of equality and apartness
 in terms of these generators.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_zero_cs.con" "CPoly_CRing__".
+inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_zero_cs.con" "CPoly_CRing__" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_linear_cs.con" "CPoly_CRing__".
+inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_linear_cs.con" "CPoly_CRing__" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0_cs.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0_cs.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ind_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ind_cs.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0_cs.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0_cs.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_zero_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_zero_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_eq_lin_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_eq_lin_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_eq_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_eq_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_lin_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_lin_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_ap_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_ap_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_comp_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_triple_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_triple_comp_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_comp_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_triple_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_triple_comp_ind.con" as lemma.
 
 (*#*
 *** The polynomials form a semi-group and a monoid
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_cs.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_plus.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_plus_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_plus_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_commutative.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_commutative.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_q_ap_q.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_q_ap_q.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_p_plus_ap_p.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_p_plus_ap_p.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero_plus.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_associative.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_associative.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csemi_grp.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csemi_grp.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cm_proof.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cm_proof.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cmonoid.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cmonoid.con" as definition.
 
 (*#* *** The polynomials form a group
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_cs.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cg_proof.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cg_proof.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cgroup.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cgroup.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cag_proof.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cag_proof.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cabgroup.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cabgroup.con" as definition.
 
 (*#* *** The polynomials form a ring
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_cs.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult_cr.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult_cr.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult_cr.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult_cr.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cs.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cs.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_dist.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_dist.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_dist.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_dist.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult_cr.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult_cr.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_lin.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_commutative.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_commutative.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_dist_rht.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_dist_rht.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_assoc.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_assoc.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_one.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_one.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one_mult.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_one.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_one.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_monoid.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_monoid.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_non_triv.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_non_triv.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CRing.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CRing.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cring.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cring.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_C_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_C_.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_X_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_X_.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con" as lemma.
 
 (* UNEXPORTED
 End CPoly_CRing
@@ -327,7 +327,7 @@ Implicit Arguments _C_ [CR].
 Implicit Arguments _X_ [CR].
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun'.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun'.con" as definition.
 
 (* UNEXPORTED
 Implicit Arguments cpoly_linear_fun' [CR].
@@ -370,55 +370,55 @@ alias id "c" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c
 
 alias id "d" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var".
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/zero_eq_linear_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/zero_eq_linear_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_eq_linear.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_eq_linear.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_linear_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_linear_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_linear.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_linear.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_ap_linear.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_ap_linear.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_linear.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_linear.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con" as lemma.
 
 (* UNEXPORTED
 End helpful_section
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_double_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_double_comp_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_triple_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_triple_comp_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_induc.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_induc.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/poly_double_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/poly_double_comp_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/poly_triple_comp_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/poly_triple_comp_ind.con" as lemma.
 
 (* UNEXPORTED
 Transparent cpoly_cring.
@@ -432,13 +432,13 @@ Transparent cpoly_cgroup.
 Transparent cpoly_csetoid.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con" as definition.
 
 (* UNEXPORTED
 End CPoly_CRing_ctd
@@ -482,23 +482,23 @@ Notation RX := (cpoly_cring R).
 *** Constant and identity
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_X_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_X_.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_C_.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_C_.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve cpoly_X_ cpoly_C_: algebra.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_const_eq.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_const_eq.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_c_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_c_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_c_one.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_c_one.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve cpoly_lin: algebra.
@@ -506,19 +506,19 @@ Hint Resolve cpoly_lin: algebra.
 
 (* SUPERFLUOUS *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/poly_linear.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/poly_linear.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve _c_zero: algebra.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/poly_c_apzero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/poly_c_apzero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_lin.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_lin.con" as lemma.
 
 (* SUPERFLUOUS ? *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/lin_mult.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/lin_mult.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve lin_mult: algebra.
@@ -527,57 +527,57 @@ Hint Resolve lin_mult: algebra.
 (*#* *** Application of polynomials
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/poly_eq_zero.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/poly_eq_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/apply_wd.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/apply_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_pres_eq.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_pres_eq.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_strext.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid_op.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid_op.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_c_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_c_apply.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_x_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_x_apply.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/plus_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/plus_apply.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/inv_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/inv_apply.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve plus_apply inv_apply: algebra.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/minus_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/minus_apply.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_apply.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve _c_mult_apply: algebra.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/mult_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/mult_apply.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve mult_apply: algebra.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/one_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/one_apply.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve one_apply: algebra.
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/nexp_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/nexp_apply.con" as lemma.
 
 (* SUPERFLUOUS *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/poly_inv_apply.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/poly_inv_apply.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Sum0_cpoly_ap.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Sum0_cpoly_ap.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con" as lemma.
 
 (* UNEXPORTED
 End Poly_properties
@@ -608,7 +608,7 @@ Notation Cpoly_linear := (cpoly_linear CR).
 Notation Cpoly_cring := (cpoly_cring CR).
 *)
 
-inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con".
+inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con" as lemma.
 
 (* UNEXPORTED
 End Poly_Prop_Induction