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