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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: CPolynomials.v,v 1.9 2004/04/23 10:00:53 lcf Exp $ *)
  20
  21 (*#* printing _X_ %\ensuremath{x}% *)
  22
  23 (*#* printing _C_ %\ensuremath\diamond% *)
  24
  25 (*#* printing [+X*] %\ensuremath{+x\times}% #+x&times;# *)
  26
  27 (*#* printing RX %\ensuremath{R[x]}% #R[x]# *)
  28
  29 (*#* printing FX %\ensuremath{F[x]}% #F[x]# *)
  30
  31 include "tactics/RingReflection.ma".
  32
  33 (*#* * Polynomials
  34 The first section only proves the polynomials form a ring, and nothing more
  35 interesting.
  36 Section%~\ref{section:poly-equality}% gives some basic properties of
  37 equality and induction of polynomials.
  38 ** Definition of polynomials; they form a ring
  39 %\label{section:poly-ring}%
  40 *)
  41
  42 (* UNEXPORTED
  43 Section CPoly_CRing
  44 *)
  45
  46 (*#*
  47 %\begin{convention}% Let [CR] be a ring.
  48 %\end{convention}%
  49 *)
  50
  51 alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/CR.var".
  52
  53 (*#*
  54 The intuition behind the type [cpoly] is the following
  55 - [(cpoly CR)] is $CR[X]$ #CR[X]#;
  56 - [cpoly_zero] is the `empty' polynomial with no coefficients;
  57 - [(cpoly_linear c p)] is [c[+]X[*]p]
  58
  59 *)
  60
  61 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly.ind".
  62
  63 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant.con" as definition.
  64
  65 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one.con" as definition.
  66
  67 (*#*
  68 Some useful induction lemmas for doubly quantified propositions.
  69 *)
  70
  71 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0.con" as lemma.
  72
  73 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0.con" as lemma.
  74
  75 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0'.con" as lemma.
  76
  77 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0.con" as lemma.
  78
  79 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0.con" as lemma.
  80
  81 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0'.con" as lemma.
  82
  83 (*#* *** The polynomials form a setoid
  84 *)
  85
  86 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_zero.con" as definition.
  87
  88 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq.con" as definition.
  89
  90 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_p_zero.con" as lemma.
  91
  92 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero.con" as definition.
  93
  94 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap.con" as definition.
  95
  96 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_p_zero.con" as lemma.
  97
  98 inline procedural "cic:/CoRN/algebra/CPolynomials/irreflexive_cpoly_ap.con" as lemma.
  99
 100 inline procedural "cic:/CoRN/algebra/CPolynomials/symmetric_cpoly_ap.con" as lemma.
 101
 102 inline procedural "cic:/CoRN/algebra/CPolynomials/cotransitive_cpoly_ap.con" as lemma.
 103
 104 inline procedural "cic:/CoRN/algebra/CPolynomials/tight_apart_cpoly_ap.con" as lemma.
 105
 106 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CSetoid.con" as lemma.
 107
 108 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid.con" as definition.
 109
 110 (*#*
 111 Now that we know that the polynomials form a setoid, we can use the
 112 notation with [ [#] ] and [ [=] ]. In order to use this notation,
 113 we introduce [cpoly_zero_cs] and [cpoly_linear_cs], so that Coq
 114 recognizes we are talking about a setoid.
 115 We formulate the induction properties and
 116 the most basic properties of equality and apartness
 117 in terms of these generators.
 118 *)
 119
 120 inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_zero_cs.con" "CPoly_CRing__" as definition.
 121
 122 inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_linear_cs.con" "CPoly_CRing__" as definition.
 123
 124 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con" as lemma.
 125
 126 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0_cs.con" as lemma.
 127
 128 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0_cs.con" as lemma.
 129
 130 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ind_cs.con" as lemma.
 131
 132 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0_cs.con" as lemma.
 133
 134 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0_cs.con" as lemma.
 135
 136 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_zero_.con" as lemma.
 137
 138 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_zero.con" as lemma.
 139
 140 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_eq_lin_.con" as lemma.
 141
 142 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_eq_lin.con" as lemma.
 143
 144 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_lin_.con" as lemma.
 145
 146 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_lin.con" as lemma.
 147
 148 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero_.con" as lemma.
 149
 150 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_zero.con" as lemma.
 151
 152 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero.con" as lemma.
 153
 154 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin_.con" as lemma.
 155
 156 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_ap_lin.con" as lemma.
 157
 158 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin.con" as lemma.
 159
 160 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin_.con" as lemma.
 161
 162 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_lin.con" as lemma.
 163
 164 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin.con" as lemma.
 165
 166 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_strext.con" as lemma.
 167
 168 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_wd.con" as lemma.
 169
 170 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun.con" as definition.
 171
 172 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_comp_ind.con" as lemma.
 173
 174 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_triple_comp_ind.con" as lemma.
 175
 176 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_comp_ind.con" as lemma.
 177
 178 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_triple_comp_ind.con" as lemma.
 179
 180 (*#*
 181 *** The polynomials form a semi-group and a monoid
 182 *)
 183
 184 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus.con" as definition.
 185
 186 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_cs.con" as definition.
 187
 188 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_plus.con" as lemma.
 189
 190 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_zero.con" as lemma.
 191
 192 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_plus_lin.con" as lemma.
 193
 194 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_commutative.con" as lemma.
 195
 196 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_q_ap_q.con" as lemma.
 197
 198 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_p_plus_ap_p.con" as lemma.
 199
 200 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero_plus.con" as lemma.
 201
 202 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_strext.con" as lemma.
 203
 204 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_wd.con" as lemma.
 205
 206 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op.con" as definition.
 207
 208 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_associative.con" as lemma.
 209
 210 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csemi_grp.con" as definition.
 211
 212 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cm_proof.con" as lemma.
 213
 214 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cmonoid.con" as definition.
 215
 216 (*#* *** The polynomials form a group
 217 *)
 218
 219 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv.con" as definition.
 220
 221 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_cs.con" as definition.
 222
 223 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_zero.con" as lemma.
 224
 225 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_lin.con" as lemma.
 226
 227 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_strext.con" as lemma.
 228
 229 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_wd.con" as lemma.
 230
 231 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op.con" as definition.
 232
 233 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cg_proof.con" as lemma.
 234
 235 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cgroup.con" as definition.
 236
 237 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cag_proof.con" as lemma.
 238
 239 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cabgroup.con" as definition.
 240
 241 (*#* *** The polynomials form a ring
 242 *)
 243
 244 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr.con" as definition.
 245
 246 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult.con" as definition.
 247
 248 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_cs.con" as definition.
 249
 250 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult_cr.con" as lemma.
 251
 252 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult_cr.con" as lemma.
 253
 254 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_zero.con" as lemma.
 255
 256 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_strext.con" as lemma.
 257
 258 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_wd.con" as lemma.
 259
 260 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cs.con" as definition.
 261
 262 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult.con" as lemma.
 263
 264 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult.con" as lemma.
 265
 266 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_strext.con" as lemma.
 267
 268 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_wd.con" as lemma.
 269
 270 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op.con" as definition.
 271
 272 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_dist.con" as lemma.
 273
 274 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_dist.con" as lemma.
 275
 276 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult_cr.con" as lemma.
 277
 278 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult.con" as lemma.
 279
 280 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_zero.con" as lemma.
 281
 282 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_lin.con" as lemma.
 283
 284 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_commutative.con" as lemma.
 285
 286 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_dist_rht.con" as lemma.
 287
 288 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_assoc.con" as lemma.
 289
 290 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_one.con" as lemma.
 291
 292 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one_mult.con" as lemma.
 293
 294 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_one.con" as lemma.
 295
 296 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_monoid.con" as lemma.
 297
 298 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_non_triv.con" as lemma.
 299
 300 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CRing.con" as lemma.
 301
 302 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cring.con" as definition.
 303
 304 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_strext.con" as lemma.
 305
 306 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_wd.con" as lemma.
 307
 308 inline procedural "cic:/CoRN/algebra/CPolynomials/_C_.con" as definition.
 309
 310 inline procedural "cic:/CoRN/algebra/CPolynomials/_X_.con" as definition.
 311
 312 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c.con" as definition.
 313
 314 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_strext.con" as lemma.
 315
 316 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con" as lemma.
 317
 318 (* UNEXPORTED
 319 End CPoly_CRing
 320 *)
 321
 322 (* UNEXPORTED
 323 Implicit Arguments _C_ [CR].
 324 *)
 325
 326 (* UNEXPORTED
 327 Implicit Arguments _X_ [CR].
 328 *)
 329
 330 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun'.con" as definition.
 331
 332 (* UNEXPORTED
 333 Implicit Arguments cpoly_linear_fun' [CR].
 334 *)
 335
 336 (* NOTATION
 337 Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
 338 *)
 339
 340 (*#* ** Apartness, equality, and induction
 341 %\label{section:poly-equality}%
 342 *)
 343
 344 (* UNEXPORTED
 345 Section CPoly_CRing_ctd
 346 *)
 347
 348 (*#*
 349 %\begin{convention}%
 350 Let [CR] be a ring, [p] and [q] polynomials over that ring, and [c] and [d]
 351 elements of the ring.
 352 %\end{convention}%
 353 *)
 354
 355 alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/CR.var".
 356
 357 (* NOTATION
 358 Notation RX := (cpoly_cring CR).
 359 *)
 360
 361 (* UNEXPORTED
 362 Section helpful_section
 363 *)
 364
 365 alias id "p" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/p.var".
 366
 367 alias id "q" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/q.var".
 368
 369 alias id "c" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c.var".
 370
 371 alias id "d" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var".
 372
 373 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con" as lemma.
 374
 375 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_zero.con" as lemma.
 376
 377 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_eq_linear_.con" as lemma.
 378
 379 inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_eq_linear.con" as lemma.
 380
 381 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_linear_.con" as lemma.
 382
 383 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_linear.con" as lemma.
 384
 385 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero_.con" as lemma.
 386
 387 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_zero.con" as lemma.
 388
 389 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero.con" as lemma.
 390
 391 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear_.con" as lemma.
 392
 393 inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_ap_linear.con" as lemma.
 394
 395 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear.con" as lemma.
 396
 397 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear_.con" as lemma.
 398
 399 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_linear.con" as lemma.
 400
 401 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con" as lemma.
 402
 403 (* UNEXPORTED
 404 End helpful_section
 405 *)
 406
 407 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con" as lemma.
 408
 409 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind.con" as lemma.
 410
 411 inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_double_comp_ind.con" as lemma.
 412
 413 inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_triple_comp_ind.con" as lemma.
 414
 415 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_induc.con" as lemma.
 416
 417 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind.con" as lemma.
 418
 419 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_double_comp_ind.con" as lemma.
 420
 421 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_triple_comp_ind.con" as lemma.
 422
 423 (* UNEXPORTED
 424 Transparent cpoly_cring.
 425 *)
 426
 427 (* UNEXPORTED
 428 Transparent cpoly_cgroup.
 429 *)
 430
 431 (* UNEXPORTED
 432 Transparent cpoly_csetoid.
 433 *)
 434
 435 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply.con" as definition.
 436
 437 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_strext.con" as lemma.
 438
 439 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_wd.con" as lemma.
 440
 441 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con" as definition.
 442
 443 (* UNEXPORTED
 444 End CPoly_CRing_ctd
 445 *)
 446
 447 (*#*
 448 %\begin{convention}%
 449 [cpoly_apply_fun] is denoted infix by [!]
 450 The first argument is left implicit, so the application of
 451 polynomial [f] (seen as a function) to argument [x] can be written as [f!x].
 452 In the names of lemmas, we write [apply].
 453 %\end{convention}%
 454 *)
 455
 456 (* UNEXPORTED
 457 Implicit Arguments cpoly_apply_fun [CR].
 458 *)
 459
 460 (* NOTATION
 461 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
 462 *)
 463
 464 (*#*
 465 ** Basic properties of polynomials
 466 %\begin{convention}%
 467 Let [R] be a ring and write [RX] for the ring of polynomials over [R].
 468 %\end{convention}%
 469 *)
 470
 471 (* UNEXPORTED
 472 Section Poly_properties
 473 *)
 474
 475 alias id "R" = "cic:/CoRN/algebra/CPolynomials/Poly_properties/R.var".
 476
 477 (* NOTATION
 478 Notation RX := (cpoly_cring R).
 479 *)
 480
 481 (*#*
 482 *** Constant and identity
 483 *)
 484
 485 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_X_.con" as lemma.
 486
 487 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_C_.con" as lemma.
 488
 489 (* UNEXPORTED
 490 Hint Resolve cpoly_X_ cpoly_C_: algebra.
 491 *)
 492
 493 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_const_eq.con" as lemma.
 494
 495 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_zero.con" as lemma.
 496
 497 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_one.con" as lemma.
 498
 499 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult.con" as lemma.
 500
 501 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin.con" as lemma.
 502
 503 (* UNEXPORTED
 504 Hint Resolve cpoly_lin: algebra.
 505 *)
 506
 507 (* SUPERFLUOUS *)
 508
 509 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_linear.con" as lemma.
 510
 511 (* UNEXPORTED
 512 Hint Resolve _c_zero: algebra.
 513 *)
 514
 515 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_c_apzero.con" as lemma.
 516
 517 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_lin.con" as lemma.
 518
 519 (* SUPERFLUOUS ? *)
 520
 521 inline procedural "cic:/CoRN/algebra/CPolynomials/lin_mult.con" as lemma.
 522
 523 (* UNEXPORTED
 524 Hint Resolve lin_mult: algebra.
 525 *)
 526
 527 (*#* *** Application of polynomials
 528 *)
 529
 530 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_eq_zero.con" as lemma.
 531
 532 inline procedural "cic:/CoRN/algebra/CPolynomials/apply_wd.con" as lemma.
 533
 534 inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_pres_eq.con" as lemma.
 535
 536 inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_strext.con" as lemma.
 537
 538 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid_op.con" as definition.
 539
 540 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_apply.con" as lemma.
 541
 542 inline procedural "cic:/CoRN/algebra/CPolynomials/_x_apply.con" as lemma.
 543
 544 inline procedural "cic:/CoRN/algebra/CPolynomials/plus_apply.con" as lemma.
 545
 546 inline procedural "cic:/CoRN/algebra/CPolynomials/inv_apply.con" as lemma.
 547
 548 (* UNEXPORTED
 549 Hint Resolve plus_apply inv_apply: algebra.
 550 *)
 551
 552 inline procedural "cic:/CoRN/algebra/CPolynomials/minus_apply.con" as lemma.
 553
 554 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_apply.con" as lemma.
 555
 556 (* UNEXPORTED
 557 Hint Resolve _c_mult_apply: algebra.
 558 *)
 559
 560 inline procedural "cic:/CoRN/algebra/CPolynomials/mult_apply.con" as lemma.
 561
 562 (* UNEXPORTED
 563 Hint Resolve mult_apply: algebra.
 564 *)
 565
 566 inline procedural "cic:/CoRN/algebra/CPolynomials/one_apply.con" as lemma.
 567
 568 (* UNEXPORTED
 569 Hint Resolve one_apply: algebra.
 570 *)
 571
 572 inline procedural "cic:/CoRN/algebra/CPolynomials/nexp_apply.con" as lemma.
 573
 574 (* SUPERFLUOUS *)
 575
 576 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_inv_apply.con" as lemma.
 577
 578 inline procedural "cic:/CoRN/algebra/CPolynomials/Sum0_cpoly_ap.con" as lemma.
 579
 580 inline procedural "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con" as lemma.
 581
 582 (* UNEXPORTED
 583 End Poly_properties
 584 *)
 585
 586 (*#* ** Induction properties of polynomials for [Prop]
 587 *)
 588
 589 (* UNEXPORTED
 590 Section Poly_Prop_Induction
 591 *)
 592
 593 alias id "CR" = "cic:/CoRN/algebra/CPolynomials/Poly_Prop_Induction/CR.var".
 594
 595 (* NOTATION
 596 Notation Cpoly := (cpoly CR).
 597 *)
 598
 599 (* NOTATION
 600 Notation Cpoly_zero := (cpoly_zero CR).
 601 *)
 602
 603 (* NOTATION
 604 Notation Cpoly_linear := (cpoly_linear CR).
 605 *)
 606
 607 (* NOTATION
 608 Notation Cpoly_cring := (cpoly_cring CR).
 609 *)
 610
 611 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con" as lemma.
 612
 613 (* UNEXPORTED
 614 End Poly_Prop_Induction
 615 *)
 616
 617 (* UNEXPORTED
 618 Hint Resolve poly_linear cpoly_lin: algebra.
 619 *)
 620
 621 (* UNEXPORTED
 622 Hint Resolve apply_wd cpoly_const_eq: algebra_c.
 623 *)
 624
 625 (* UNEXPORTED
 626 Hint Resolve _c_apply _x_apply inv_apply plus_apply minus_apply mult_apply
 627   nexp_apply: algebra.
 628 *)
 629
 630 (* UNEXPORTED
 631 Hint Resolve one_apply _c_zero _c_one _c_mult: algebra.
 632 *)
 633
 634 (* UNEXPORTED
 635 Hint Resolve poly_inv_apply: algebra.
 636 *)
 637
 638 (* UNEXPORTED
 639 Hint Resolve _c_mult_lin: algebra.
 640 *)
 641