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 inline "cic:/CoRN/algebra/CPolynomials/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_zero_cs.con".
 123
 124 inline "cic:/CoRN/algebra/CPolynomials/cpoly_linear_cs.con".
 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 (*#* ** Apartness, equality, and induction
 339 %\label{section:poly-equality}%
 340 *)
 341
 342 (* UNEXPORTED
 343 Section CPoly_CRing_ctd.
 344 *)
 345
 346 (*#*
 347 %\begin{convention}%
 348 Let [CR] be a ring, [p] and [q] polynomials over that ring, and [c] and [d]
 349 elements of the ring.
 350 %\end{convention}%
 351 *)
 352
 353 inline "cic:/CoRN/algebra/CPolynomials/CR.var".
 354
 355 (* UNEXPORTED
 356 Section helpful_section.
 357 *)
 358
 359 inline "cic:/CoRN/algebra/CPolynomials/p.var".
 360
 361 inline "cic:/CoRN/algebra/CPolynomials/q.var".
 362
 363 inline "cic:/CoRN/algebra/CPolynomials/c.var".
 364
 365 inline "cic:/CoRN/algebra/CPolynomials/d.var".
 366
 367 inline "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con".
 368
 369 inline "cic:/CoRN/algebra/CPolynomials/_linear_eq_zero.con".
 370
 371 inline "cic:/CoRN/algebra/CPolynomials/zero_eq_linear_.con".
 372
 373 inline "cic:/CoRN/algebra/CPolynomials/_zero_eq_linear.con".
 374
 375 inline "cic:/CoRN/algebra/CPolynomials/linear_eq_linear_.con".
 376
 377 inline "cic:/CoRN/algebra/CPolynomials/_linear_eq_linear.con".
 378
 379 inline "cic:/CoRN/algebra/CPolynomials/linear_ap_zero_.con".
 380
 381 inline "cic:/CoRN/algebra/CPolynomials/_linear_ap_zero.con".
 382
 383 inline "cic:/CoRN/algebra/CPolynomials/linear_ap_zero.con".
 384
 385 inline "cic:/CoRN/algebra/CPolynomials/zero_ap_linear_.con".
 386
 387 inline "cic:/CoRN/algebra/CPolynomials/_zero_ap_linear.con".
 388
 389 inline "cic:/CoRN/algebra/CPolynomials/zero_ap_linear.con".
 390
 391 inline "cic:/CoRN/algebra/CPolynomials/linear_ap_linear_.con".
 392
 393 inline "cic:/CoRN/algebra/CPolynomials/_linear_ap_linear.con".
 394
 395 inline "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con".
 396
 397 (* UNEXPORTED
 398 End helpful_section.
 399 *)
 400
 401 inline "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con".
 402
 403 inline "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind.con".
 404
 405 inline "cic:/CoRN/algebra/CPolynomials/Cpoly_double_comp_ind.con".
 406
 407 inline "cic:/CoRN/algebra/CPolynomials/Cpoly_triple_comp_ind.con".
 408
 409 inline "cic:/CoRN/algebra/CPolynomials/cpoly_induc.con".
 410
 411 inline "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind.con".
 412
 413 inline "cic:/CoRN/algebra/CPolynomials/poly_double_comp_ind.con".
 414
 415 inline "cic:/CoRN/algebra/CPolynomials/poly_triple_comp_ind.con".
 416
 417 (* UNEXPORTED
 418 Transparent cpoly_cring.
 419 *)
 420
 421 (* UNEXPORTED
 422 Transparent cpoly_cgroup.
 423 *)
 424
 425 (* UNEXPORTED
 426 Transparent cpoly_csetoid.
 427 *)
 428
 429 inline "cic:/CoRN/algebra/CPolynomials/cpoly_apply.con".
 430
 431 inline "cic:/CoRN/algebra/CPolynomials/cpoly_apply_strext.con".
 432
 433 inline "cic:/CoRN/algebra/CPolynomials/cpoly_apply_wd.con".
 434
 435 inline "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con".
 436
 437 (* UNEXPORTED
 438 End CPoly_CRing_ctd.
 439 *)
 440
 441 (*#*
 442 %\begin{convention}%
 443 [cpoly_apply_fun] is denoted infix by [!]
 444 The first argument is left implicit, so the application of
 445 polynomial [f] (seen as a function) to argument [x] can be written as [f!x].
 446 In the names of lemmas, we write [apply].
 447 %\end{convention}%
 448 *)
 449
 450 (* UNEXPORTED
 451 Implicit Arguments cpoly_apply_fun [CR].
 452 *)
 453
 454 (*#*
 455 ** Basic properties of polynomials
 456 %\begin{convention}%
 457 Let [R] be a ring and write [RX] for the ring of polynomials over [R].
 458 %\end{convention}%
 459 *)
 460
 461 (* UNEXPORTED
 462 Section Poly_properties.
 463 *)
 464
 465 inline "cic:/CoRN/algebra/CPolynomials/R.var".
 466
 467 (*#*
 468 *** Constant and identity
 469 *)
 470
 471 inline "cic:/CoRN/algebra/CPolynomials/cpoly_X_.con".
 472
 473 inline "cic:/CoRN/algebra/CPolynomials/cpoly_C_.con".
 474
 475 (* UNEXPORTED
 476 Hint Resolve cpoly_X_ cpoly_C_: algebra.
 477 *)
 478
 479 inline "cic:/CoRN/algebra/CPolynomials/cpoly_const_eq.con".
 480
 481 inline "cic:/CoRN/algebra/CPolynomials/_c_zero.con".
 482
 483 inline "cic:/CoRN/algebra/CPolynomials/_c_one.con".
 484
 485 inline "cic:/CoRN/algebra/CPolynomials/_c_mult.con".
 486
 487 inline "cic:/CoRN/algebra/CPolynomials/cpoly_lin.con".
 488
 489 (* UNEXPORTED
 490 Hint Resolve cpoly_lin: algebra.
 491 *)
 492
 493 (* SUPERFLUOUS *)
 494
 495 inline "cic:/CoRN/algebra/CPolynomials/poly_linear.con".
 496
 497 (* UNEXPORTED
 498 Hint Resolve _c_zero: algebra.
 499 *)
 500
 501 inline "cic:/CoRN/algebra/CPolynomials/poly_c_apzero.con".
 502
 503 inline "cic:/CoRN/algebra/CPolynomials/_c_mult_lin.con".
 504
 505 (* SUPERFLUOUS ? *)
 506
 507 inline "cic:/CoRN/algebra/CPolynomials/lin_mult.con".
 508
 509 (* UNEXPORTED
 510 Hint Resolve lin_mult: algebra.
 511 *)
 512
 513 (*#* *** Application of polynomials
 514 *)
 515
 516 inline "cic:/CoRN/algebra/CPolynomials/poly_eq_zero.con".
 517
 518 inline "cic:/CoRN/algebra/CPolynomials/apply_wd.con".
 519
 520 inline "cic:/CoRN/algebra/CPolynomials/cpolyap_pres_eq.con".
 521
 522 inline "cic:/CoRN/algebra/CPolynomials/cpolyap_strext.con".
 523
 524 inline "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid_op.con".
 525
 526 inline "cic:/CoRN/algebra/CPolynomials/_c_apply.con".
 527
 528 inline "cic:/CoRN/algebra/CPolynomials/_x_apply.con".
 529
 530 inline "cic:/CoRN/algebra/CPolynomials/plus_apply.con".
 531
 532 inline "cic:/CoRN/algebra/CPolynomials/inv_apply.con".
 533
 534 (* UNEXPORTED
 535 Hint Resolve plus_apply inv_apply: algebra.
 536 *)
 537
 538 inline "cic:/CoRN/algebra/CPolynomials/minus_apply.con".
 539
 540 inline "cic:/CoRN/algebra/CPolynomials/_c_mult_apply.con".
 541
 542 (* UNEXPORTED
 543 Hint Resolve _c_mult_apply: algebra.
 544 *)
 545
 546 inline "cic:/CoRN/algebra/CPolynomials/mult_apply.con".
 547
 548 (* UNEXPORTED
 549 Hint Resolve mult_apply: algebra.
 550 *)
 551
 552 inline "cic:/CoRN/algebra/CPolynomials/one_apply.con".
 553
 554 (* UNEXPORTED
 555 Hint Resolve one_apply: algebra.
 556 *)
 557
 558 inline "cic:/CoRN/algebra/CPolynomials/nexp_apply.con".
 559
 560 (* SUPERFLUOUS *)
 561
 562 inline "cic:/CoRN/algebra/CPolynomials/poly_inv_apply.con".
 563
 564 inline "cic:/CoRN/algebra/CPolynomials/Sum0_cpoly_ap.con".
 565
 566 inline "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con".
 567
 568 (* UNEXPORTED
 569 End Poly_properties.
 570 *)
 571
 572 (*#* ** Induction properties of polynomials for [Prop]
 573 *)
 574
 575 (* UNEXPORTED
 576 Section Poly_Prop_Induction.
 577 *)
 578
 579 inline "cic:/CoRN/algebra/CPolynomials/CR.var".
 580
 581 inline "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con".
 582
 583 (* UNEXPORTED
 584 End Poly_Prop_Induction.
 585 *)
 586
 587 (* UNEXPORTED
 588 Hint Resolve poly_linear cpoly_lin: algebra.
 589 *)
 590
 591 (* UNEXPORTED
 592 Hint Resolve apply_wd cpoly_const_eq: algebra_c.
 593 *)
 594
 595 (* UNEXPORTED
 596 Hint Resolve _c_apply _x_apply inv_apply plus_apply minus_apply mult_apply
 597   nexp_apply: algebra.
 598 *)
 599
 600 (* UNEXPORTED
 601 Hint Resolve one_apply _c_zero _c_one _c_mult: algebra.
 602 *)
 603
 604 (* UNEXPORTED
 605 Hint Resolve poly_inv_apply: algebra.
 606 *)
 607
 608 (* UNEXPORTED
 609 Hint Resolve _c_mult_lin: algebra.
 610 *)
 611