Pour les règles d'introduction, j'ai utilisé la commodité offerte par $\perp$:
la dérivation reçoit une fonction $f: R-> Rperp$ et retourne une fonction $f'$
du même type. Et bien sûr, $f $ est dérivable là où $f'$ ne vaut pas $\perp$.
Ce point de vue permet de parler de $f'(x)$ avant de savoir si $f$ est
dérivable en $x$, et de définir sans contorsions les dérivées
supérieures.
Les règles de reproduction sont comme d'hab (opérations algébriques, composée, réciproque).
Pour les règles d'élimination, j'ai tout centré sur la formule de Taylor-Lagrange, qui sait produire une inégalité sur la fonction à partir d'une inégalité sur une de ses dérivées. En effet, comme cas particulier à l'ordre $0$, on a le coup du sens de variation et la formule des accroissements finis et à l'ordre $1$, le coup de la convexité. Et j'ai expliqué comment cette formule s'applique aux fonctions usuelles, voir l'exo-type 8 (tex, ps, pdf).