matita/contribs/CoRN-Decl/algebra/CPolynomials.ma

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