matita/matita/contribs/procedural/CoRN/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 (* UNEXPORTED
  52 cic:/CoRN/algebra/CPolynomials/CPoly_CRing/CR.var
  53 *)
  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 procedural "cic:/CoRN/algebra/CPolynomials/cpoly.ind".
  64
  65 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant.con" as definition.
  66
  67 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one.con" as definition.
  68
  69 (*#*
  70 Some useful induction lemmas for doubly quantified propositions.
  71 *)
  72
  73 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0.con" as lemma.
  74
  75 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0.con" as lemma.
  76
  77 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0'.con" as lemma.
  78
  79 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0.con" as lemma.
  80
  81 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0.con" as lemma.
  82
  83 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0'.con" as lemma.
  84
  85 (*#* *** The polynomials form a setoid
  86 *)
  87
  88 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_zero.con" as definition.
  89
  90 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq.con" as definition.
  91
  92 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_p_zero.con" as lemma.
  93
  94 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero.con" as definition.
  95
  96 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap.con" as definition.
  97
  98 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_p_zero.con" as lemma.
  99
 100 inline procedural "cic:/CoRN/algebra/CPolynomials/irreflexive_cpoly_ap.con" as lemma.
 101
 102 inline procedural "cic:/CoRN/algebra/CPolynomials/symmetric_cpoly_ap.con" as lemma.
 103
 104 inline procedural "cic:/CoRN/algebra/CPolynomials/cotransitive_cpoly_ap.con" as lemma.
 105
 106 inline procedural "cic:/CoRN/algebra/CPolynomials/tight_apart_cpoly_ap.con" as lemma.
 107
 108 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CSetoid.con" as lemma.
 109
 110 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid.con" as definition.
 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 procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_zero_cs.con" "CPoly_CRing__" as definition.
 123
 124 inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_linear_cs.con" "CPoly_CRing__" as definition.
 125
 126 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con" as lemma.
 127
 128 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0_cs.con" as lemma.
 129
 130 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0_cs.con" as lemma.
 131
 132 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ind_cs.con" as lemma.
 133
 134 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0_cs.con" as lemma.
 135
 136 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0_cs.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_lin_eq_zero.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_zero_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_eq_lin.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_lin_ap_zero.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_zero_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_lin_ap_lin.con" as lemma.
 167
 168 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_strext.con" as lemma.
 169
 170 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_wd.con" as lemma.
 171
 172 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun.con" as definition.
 173
 174 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_comp_ind.con" as lemma.
 175
 176 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_triple_comp_ind.con" as lemma.
 177
 178 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_comp_ind.con" as lemma.
 179
 180 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_triple_comp_ind.con" as lemma.
 181
 182 (*#*
 183 *** The polynomials form a semi-group and a monoid
 184 *)
 185
 186 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus.con" as definition.
 187
 188 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_cs.con" as definition.
 189
 190 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_plus.con" as lemma.
 191
 192 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_zero.con" as lemma.
 193
 194 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_plus_lin.con" as lemma.
 195
 196 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_commutative.con" as lemma.
 197
 198 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_q_ap_q.con" as lemma.
 199
 200 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_p_plus_ap_p.con" as lemma.
 201
 202 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero_plus.con" as lemma.
 203
 204 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_strext.con" as lemma.
 205
 206 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_wd.con" as lemma.
 207
 208 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op.con" as definition.
 209
 210 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_associative.con" as lemma.
 211
 212 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csemi_grp.con" as definition.
 213
 214 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cm_proof.con" as lemma.
 215
 216 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cmonoid.con" as definition.
 217
 218 (*#* *** The polynomials form a group
 219 *)
 220
 221 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv.con" as definition.
 222
 223 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_cs.con" as definition.
 224
 225 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_zero.con" as lemma.
 226
 227 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_lin.con" as lemma.
 228
 229 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_strext.con" as lemma.
 230
 231 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_wd.con" as lemma.
 232
 233 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op.con" as definition.
 234
 235 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cg_proof.con" as lemma.
 236
 237 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cgroup.con" as definition.
 238
 239 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cag_proof.con" as lemma.
 240
 241 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cabgroup.con" as definition.
 242
 243 (*#* *** The polynomials form a ring
 244 *)
 245
 246 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr.con" as definition.
 247
 248 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult.con" as definition.
 249
 250 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_cs.con" as definition.
 251
 252 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult_cr.con" as lemma.
 253
 254 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult_cr.con" as lemma.
 255
 256 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_zero.con" as lemma.
 257
 258 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_strext.con" as lemma.
 259
 260 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_wd.con" as lemma.
 261
 262 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cs.con" as definition.
 263
 264 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult.con" as lemma.
 265
 266 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult.con" as lemma.
 267
 268 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_strext.con" as lemma.
 269
 270 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_wd.con" as lemma.
 271
 272 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op.con" as definition.
 273
 274 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_dist.con" as lemma.
 275
 276 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_dist.con" as lemma.
 277
 278 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult_cr.con" as lemma.
 279
 280 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult.con" as lemma.
 281
 282 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_zero.con" as lemma.
 283
 284 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_lin.con" as lemma.
 285
 286 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_commutative.con" as lemma.
 287
 288 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_dist_rht.con" as lemma.
 289
 290 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_assoc.con" as lemma.
 291
 292 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_one.con" as lemma.
 293
 294 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one_mult.con" as lemma.
 295
 296 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_one.con" as lemma.
 297
 298 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_monoid.con" as lemma.
 299
 300 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_non_triv.con" as lemma.
 301
 302 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CRing.con" as lemma.
 303
 304 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cring.con" as definition.
 305
 306 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_strext.con" as lemma.
 307
 308 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_wd.con" as lemma.
 309
 310 inline procedural "cic:/CoRN/algebra/CPolynomials/_C_.con" as definition.
 311
 312 inline procedural "cic:/CoRN/algebra/CPolynomials/_X_.con" as definition.
 313
 314 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c.con" as definition.
 315
 316 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_strext.con" as lemma.
 317
 318 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con" as lemma.
 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 procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun'.con" as definition.
 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 (* UNEXPORTED
 358 cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/CR.var
 359 *)
 360
 361 (* NOTATION
 362 Notation RX := (cpoly_cring CR).
 363 *)
 364
 365 (* UNEXPORTED
 366 Section helpful_section
 367 *)
 368
 369 (* UNEXPORTED
 370 cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/p.var
 371 *)
 372
 373 (* UNEXPORTED
 374 cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/q.var
 375 *)
 376
 377 (* UNEXPORTED
 378 cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c.var
 379 *)
 380
 381 (* UNEXPORTED
 382 cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var
 383 *)
 384
 385 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con" as lemma.
 386
 387 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_zero.con" as lemma.
 388
 389 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_eq_linear_.con" as lemma.
 390
 391 inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_eq_linear.con" as lemma.
 392
 393 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_linear_.con" as lemma.
 394
 395 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_linear.con" as lemma.
 396
 397 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero_.con" as lemma.
 398
 399 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_zero.con" as lemma.
 400
 401 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero.con" as lemma.
 402
 403 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear_.con" as lemma.
 404
 405 inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_ap_linear.con" as lemma.
 406
 407 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear.con" as lemma.
 408
 409 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear_.con" as lemma.
 410
 411 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_linear.con" as lemma.
 412
 413 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con" as lemma.
 414
 415 (* UNEXPORTED
 416 End helpful_section
 417 *)
 418
 419 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con" as lemma.
 420
 421 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind.con" as lemma.
 422
 423 inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_double_comp_ind.con" as lemma.
 424
 425 inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_triple_comp_ind.con" as lemma.
 426
 427 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_induc.con" as lemma.
 428
 429 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind.con" as lemma.
 430
 431 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_double_comp_ind.con" as lemma.
 432
 433 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_triple_comp_ind.con" as lemma.
 434
 435 (* UNEXPORTED
 436 Transparent cpoly_cring.
 437 *)
 438
 439 (* UNEXPORTED
 440 Transparent cpoly_cgroup.
 441 *)
 442
 443 (* UNEXPORTED
 444 Transparent cpoly_csetoid.
 445 *)
 446
 447 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply.con" as definition.
 448
 449 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_strext.con" as lemma.
 450
 451 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_wd.con" as lemma.
 452
 453 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con" as definition.
 454
 455 (* UNEXPORTED
 456 End CPoly_CRing_ctd
 457 *)
 458
 459 (*#*
 460 %\begin{convention}%
 461 [cpoly_apply_fun] is denoted infix by [!]
 462 The first argument is left implicit, so the application of
 463 polynomial [f] (seen as a function) to argument [x] can be written as [f!x].
 464 In the names of lemmas, we write [apply].
 465 %\end{convention}%
 466 *)
 467
 468 (* UNEXPORTED
 469 Implicit Arguments cpoly_apply_fun [CR].
 470 *)
 471
 472 (* NOTATION
 473 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
 474 *)
 475
 476 (*#*
 477 ** Basic properties of polynomials
 478 %\begin{convention}%
 479 Let [R] be a ring and write [RX] for the ring of polynomials over [R].
 480 %\end{convention}%
 481 *)
 482
 483 (* UNEXPORTED
 484 Section Poly_properties
 485 *)
 486
 487 (* UNEXPORTED
 488 cic:/CoRN/algebra/CPolynomials/Poly_properties/R.var
 489 *)
 490
 491 (* NOTATION
 492 Notation RX := (cpoly_cring R).
 493 *)
 494
 495 (*#*
 496 *** Constant and identity
 497 *)
 498
 499 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_X_.con" as lemma.
 500
 501 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_C_.con" as lemma.
 502
 503 (* UNEXPORTED
 504 Hint Resolve cpoly_X_ cpoly_C_: algebra.
 505 *)
 506
 507 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_const_eq.con" as lemma.
 508
 509 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_zero.con" as lemma.
 510
 511 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_one.con" as lemma.
 512
 513 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult.con" as lemma.
 514
 515 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin.con" as lemma.
 516
 517 (* UNEXPORTED
 518 Hint Resolve cpoly_lin: algebra.
 519 *)
 520
 521 (* SUPERFLUOUS *)
 522
 523 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_linear.con" as lemma.
 524
 525 (* UNEXPORTED
 526 Hint Resolve _c_zero: algebra.
 527 *)
 528
 529 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_c_apzero.con" as lemma.
 530
 531 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_lin.con" as lemma.
 532
 533 (* SUPERFLUOUS ? *)
 534
 535 inline procedural "cic:/CoRN/algebra/CPolynomials/lin_mult.con" as lemma.
 536
 537 (* UNEXPORTED
 538 Hint Resolve lin_mult: algebra.
 539 *)
 540
 541 (*#* *** Application of polynomials
 542 *)
 543
 544 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_eq_zero.con" as lemma.
 545
 546 inline procedural "cic:/CoRN/algebra/CPolynomials/apply_wd.con" as lemma.
 547
 548 inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_pres_eq.con" as lemma.
 549
 550 inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_strext.con" as lemma.
 551
 552 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid_op.con" as definition.
 553
 554 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_apply.con" as lemma.
 555
 556 inline procedural "cic:/CoRN/algebra/CPolynomials/_x_apply.con" as lemma.
 557
 558 inline procedural "cic:/CoRN/algebra/CPolynomials/plus_apply.con" as lemma.
 559
 560 inline procedural "cic:/CoRN/algebra/CPolynomials/inv_apply.con" as lemma.
 561
 562 (* UNEXPORTED
 563 Hint Resolve plus_apply inv_apply: algebra.
 564 *)
 565
 566 inline procedural "cic:/CoRN/algebra/CPolynomials/minus_apply.con" as lemma.
 567
 568 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_apply.con" as lemma.
 569
 570 (* UNEXPORTED
 571 Hint Resolve _c_mult_apply: algebra.
 572 *)
 573
 574 inline procedural "cic:/CoRN/algebra/CPolynomials/mult_apply.con" as lemma.
 575
 576 (* UNEXPORTED
 577 Hint Resolve mult_apply: algebra.
 578 *)
 579
 580 inline procedural "cic:/CoRN/algebra/CPolynomials/one_apply.con" as lemma.
 581
 582 (* UNEXPORTED
 583 Hint Resolve one_apply: algebra.
 584 *)
 585
 586 inline procedural "cic:/CoRN/algebra/CPolynomials/nexp_apply.con" as lemma.
 587
 588 (* SUPERFLUOUS *)
 589
 590 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_inv_apply.con" as lemma.
 591
 592 inline procedural "cic:/CoRN/algebra/CPolynomials/Sum0_cpoly_ap.con" as lemma.
 593
 594 inline procedural "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con" as lemma.
 595
 596 (* UNEXPORTED
 597 End Poly_properties
 598 *)
 599
 600 (*#* ** Induction properties of polynomials for [Prop]
 601 *)
 602
 603 (* UNEXPORTED
 604 Section Poly_Prop_Induction
 605 *)
 606
 607 (* UNEXPORTED
 608 cic:/CoRN/algebra/CPolynomials/Poly_Prop_Induction/CR.var
 609 *)
 610
 611 (* NOTATION
 612 Notation Cpoly := (cpoly CR).
 613 *)
 614
 615 (* NOTATION
 616 Notation Cpoly_zero := (cpoly_zero CR).
 617 *)
 618
 619 (* NOTATION
 620 Notation Cpoly_linear := (cpoly_linear CR).
 621 *)
 622
 623 (* NOTATION
 624 Notation Cpoly_cring := (cpoly_cring CR).
 625 *)
 626
 627 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con" as lemma.
 628
 629 (* UNEXPORTED
 630 End Poly_Prop_Induction
 631 *)
 632
 633 (* UNEXPORTED
 634 Hint Resolve poly_linear cpoly_lin: algebra.
 635 *)
 636
 637 (* UNEXPORTED
 638 Hint Resolve apply_wd cpoly_const_eq: algebra_c.
 639 *)
 640
 641 (* UNEXPORTED
 642 Hint Resolve _c_apply _x_apply inv_apply plus_apply minus_apply mult_apply
 643   nexp_apply: algebra.
 644 *)
 645
 646 (* UNEXPORTED
 647 Hint Resolve one_apply _c_zero _c_one _c_mult: algebra.
 648 *)
 649
 650 (* UNEXPORTED
 651 Hint Resolve poly_inv_apply: algebra.
 652 *)
 653
 654 (* UNEXPORTED
 655 Hint Resolve _c_mult_lin: algebra.
 656 *)
 657