]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
[helm.git] / matitaB / matita / contribs / CoRN-Decl / ftc / MoreFunctions.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/ftc/MoreFunctions".
18
19 include "CoRN.ma".
20
21 (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
22
23 (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *)
24
25 include "ftc/MoreIntervals.ma".
26
27 (* UNEXPORTED
28 Opaque Min Max.
29 *)
30
31 (* UNEXPORTED
32 Section Basic_Results
33 *)
34
35 (*#* *More about Functions
36
37 Here we state all the main results about properties of functions that
38 we already proved for compact intervals in the more general setting of
39 arbitrary intervals.
40
41 %\begin{convention}% Let [I:interval] and [F,F',G,G'] be partial functions.
42 %\end{convention}%
43
44 **Continuity
45 *)
46
47 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var".
48
49 (*#*
50 Trivial stuff.
51 *)
52
53 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con".
54
55 (*#*
56 %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I].
57 %\end{convention}%
58 *)
59
60 alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var".
61
62 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var".
63
64 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var".
65
66 inline "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con".
67
68 (* begin show *)
69
70 alias id "Hinc" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var".
71
72 (* end show *)
73
74 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con".
75
76 inline "cic:/CoRN/ftc/MoreFunctions/FNorm.con".
77
78 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con".
79
80 (* UNEXPORTED
81 End Basic_Results
82 *)
83
84 (* UNEXPORTED
85 Hint Resolve Continuous_imp_inc: included.
86 *)
87
88 (* UNEXPORTED
89 Section Other_Results
90 *)
91
92 (*#*
93 The usual stuff.
94 *)
95
96 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var".
97
98 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var".
99
100 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var".
101
102 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con".
103
104 (* begin show *)
105
106 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var".
107
108 alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var".
109
110 (* end show *)
111
112 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con".
113
114 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con".
115
116 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con".
117
118 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con".
119
120 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con".
121
122 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con".
123
124 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con".
125
126 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con".
127
128 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con".
129
130 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con".
131
132 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con".
133
134 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con".
135
136 (* UNEXPORTED
137 End Other_Results
138 *)
139
140 (* UNEXPORTED
141 Hint Resolve continuous_compact Continuous_const Continuous_id
142   Continuous_plus Continuous_inv Continuous_minus Continuous_mult
143   Continuous_scal Continuous_nth Continuous_recip Continuous_abs: continuous.
144 *)
145
146 (* UNEXPORTED
147 Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
148 *)
149
150 (* UNEXPORTED
151 Section Corollaries
152 *)
153
154 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var".
155
156 alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var".
157
158 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var".
159
160 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var".
161
162 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var".
163
164 alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var".
165
166 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con".
167
168 inline "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con".
169
170 (* UNEXPORTED
171 End Corollaries
172 *)
173
174 (* UNEXPORTED
175 Hint Resolve Continuous_div: continuous.
176 *)
177
178 (* UNEXPORTED
179 Section Sums
180 *)
181
182 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Sums/I.var".
183
184 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con".
185
186 (*#*
187 %\begin{convention}% Assume [f] is a sequence of continuous functions.
188 %\end{convention}%
189 *)
190
191 alias id "f" = "cic:/CoRN/ftc/MoreFunctions/Sums/f.var".
192
193 alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Sums/contF.var".
194
195 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con".
196
197 inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con".
198
199 (* UNEXPORTED
200 End Sums
201 *)
202
203 (* UNEXPORTED
204 Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous.
205 *)
206
207 (* UNEXPORTED
208 Section Basic_Properties
209 *)
210
211 (*#* **Derivative
212
213 Derivative is not that much different.
214
215 %\begin{convention}% From this point on we assume [I] to be proper.
216 %\end{convention}%
217 *)
218
219 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var".
220
221 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var".
222
223 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var".
224
225 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var".
226
227 alias id "H" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var".
228
229 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con".
230
231 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con".
232
233 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con".
234
235 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con".
236
237 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con".
238
239 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con".
240
241 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con".
242
243 (* UNEXPORTED
244 End Basic_Properties
245 *)
246
247 (* UNEXPORTED
248 Hint Immediate Derivative_imp_inc Derivative_imp_inc': included.
249 *)
250
251 (* UNEXPORTED
252 Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
253   continuous.
254 *)
255
256 (* UNEXPORTED
257 Section More_Results
258 *)
259
260 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Results/I.var".
261
262 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var".
263
264 (*#*
265 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
266 %\end{convention}%
267 *)
268
269 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F.var".
270
271 alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var".
272
273 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G.var".
274
275 alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var".
276
277 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var".
278
279 alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var".
280
281 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con".
282
283 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con".
284
285 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con".
286
287 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con".
288
289 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con".
290
291 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con".
292
293 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con".
294
295 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con".
296
297 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con".
298
299 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con".
300
301 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con".
302
303 (* UNEXPORTED
304 End More_Results
305 *)
306
307 (* UNEXPORTED
308 Section More_Corollaries
309 *)
310
311 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var".
312
313 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var".
314
315 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var".
316
317 alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var".
318
319 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var".
320
321 alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var".
322
323 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var".
324
325 alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var".
326
327 (* begin show *)
328
329 alias id "Gbnd" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var".
330
331 (* end show *)
332
333 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con".
334
335 (* UNEXPORTED
336 End More_Corollaries
337 *)
338
339 (* UNEXPORTED
340 Section More_Sums
341 *)
342
343 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var".
344
345 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var".
346
347 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con".
348
349 (* begin show *)
350
351 alias id "f" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var".
352
353 alias id "f'" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var".
354
355 alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var".
356
357 (* end show *)
358
359 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con".
360
361 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con".
362
363 (* UNEXPORTED
364 End More_Sums
365 *)
366
367 (* UNEXPORTED
368 Section Diffble_Basic_Properties
369 *)
370
371 (*#* **Differentiability
372
373 Mutatis mutandis for differentiability.
374 *)
375
376 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var".
377
378 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var".
379
380 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con".
381
382 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con".
383
384 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con".
385
386 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var".
387
388 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var".
389
390 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var".
391
392 alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var".
393
394 (*#*
395 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
396 %\end{convention}%
397 *)
398
399 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con".
400
401 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con".
402
403 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con".
404
405 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con".
406
407 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con".
408
409 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con".
410
411 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con".
412
413 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con".
414
415 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con".
416
417 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con".
418
419 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con".
420
421 (* UNEXPORTED
422 End Diffble_Basic_Properties
423 *)
424
425 (* UNEXPORTED
426 Hint Immediate Diffble_imp_inc: included.
427 *)
428
429 (* UNEXPORTED
430 Section Diffble_Corollaries
431 *)
432
433 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var".
434
435 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var".
436
437 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var".
438
439 alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var".
440
441 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var".
442
443 alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var".
444
445 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con".
446
447 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con".
448
449 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con".
450
451 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con".
452
453 (* UNEXPORTED
454 End Diffble_Corollaries
455 *)
456
457 (* UNEXPORTED
458 Section Nth_Derivative
459 *)
460
461 (*#* **Nth Derivative
462
463 Higher order derivatives pose more interesting problems.  It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
464 *)
465
466 alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var".
467
468 alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var".
469
470 (* UNEXPORTED
471 Section Definitions
472 *)
473
474 (*#*
475 %\begin{convention}% Let [n:nat], [F:PartIR] and assume that [F] is n-times differentiable in [I].
476 %\end{convention}%
477 *)
478
479 alias id "n" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var".
480
481 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var".
482
483 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var".
484
485 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con".
486
487 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char
488  (* begin hide *).con".
489
490 (* end hide *)
491
492 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con".
493
494 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con".
495
496 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con".
497
498 (* UNEXPORTED
499 End Definitions
500 *)
501
502 (* UNEXPORTED
503 Section Basic_Results
504 *)
505
506 (*#*
507 All the usual results hold.
508 *)
509
510 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con".
511
512 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con".
513
514 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con".
515
516 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con".
517
518 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con".
519
520 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con".
521
522 inline "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con".
523
524 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con".
525
526 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con".
527
528 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con".
529
530 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con".
531
532 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con".
533
534 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con".
535
536 inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con".
537
538 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con".
539
540 inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con".
541
542 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con".
543
544 (* UNEXPORTED
545 End Basic_Results
546 *)
547
548 (* UNEXPORTED
549 Section More_Results
550 *)
551
552 (*#*
553 Some new results hold, too:
554 *)
555
556 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con".
557
558 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con".
559
560 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con".
561
562 inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con".
563
564 (*#*
565 Some useful characterization results.
566 *)
567
568 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con".
569
570 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con".
571
572 (* UNEXPORTED
573 End More_Results
574 *)
575
576 (* UNEXPORTED
577 Section Derivating_Diffble
578 *)
579
580 (*#*
581 As a special case we get a differentiation operator%\ldots%#...#
582 *)
583
584 alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var".
585
586 (* begin show *)
587
588 alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var".
589
590 (* end show *)
591
592 inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con".
593
594 inline "cic:/CoRN/ftc/MoreFunctions/Deriv.con".
595
596 (* UNEXPORTED
597 End Derivating_Diffble
598 *)
599
600 (* UNEXPORTED
601 Section Corollaries
602 *)
603
604 (*#*
605 %\ldots%#...# for which the expected property also holds.
606 *)
607
608 inline "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con".
609
610 (*#*
611 Some more interesting properties.
612 *)
613
614 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con".
615
616 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con".
617
618 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con".
619
620 inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con".
621
622 (* UNEXPORTED
623 End Corollaries
624 *)
625
626 (* UNEXPORTED
627 End Nth_Derivative
628 *)
629
630 (* UNEXPORTED
631 Hint Resolve Derivative_const Derivative_id Derivative_plus Derivative_inv
632   Derivative_minus Derivative_mult Derivative_scal Derivative_nth
633   Derivative_recip Derivative_div Derivative_Sumx Derivative_Sum0
634   Derivative_Sum: derivate.
635 *)
636
637 (* UNEXPORTED
638 Hint Immediate Derivative_n_imp_inc Derivative_n_imp_inc' Diffble_n_imp_inc:
639   included.
640 *)
641
642 (* UNEXPORTED
643 Hint Resolve Deriv_lemma N_Deriv_lemma: derivate.
644 *)
645
646 (* UNEXPORTED
647 Hint Immediate Derivative_n_imp_Continuous Derivative_n_imp_Continuous':
648   continuous.
649 *)
650