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 (* $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
  32 RingReflection
  33 *)
  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