]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/algebra/CPolynomials.mma
made executable again
[helm.git] / 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×# *)
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