fact: Fixpoint symbPF_deriv (r : symbPF) : PartIR := match r with | shyp _ _ _ f' _ => f' | shyp' J pJ F H => Deriv J pJ F H | sconst c => [-C-][0] | sid => [-C-][1] | splus f g => symbPF_deriv f{+}symbPF_deriv g | sinv f => {--}(symbPF_deriv f) | sminus f g => symbPF_deriv f{-}symbPF_deriv g | smult f g => symb_to_PartIR f{*}symbPF_deriv g{+}symbPF_deriv f{*}symb_to_PartIR g | sscalmult c f => c{**}symbPF_deriv f | snth f n => match n with | O => [-C-][0] | S p => nring (S p){**}(symbPF_deriv f{*}symb_to_PartIR (snth f p)) end | srecip f => {--}(symbPF_deriv f{/}symb_to_PartIR f{*}symb_to_PartIR f) | sdiv f g => (symbPF_deriv f{*}symb_to_PartIR g{-}symb_to_PartIR f{*}symbPF_deriv g){/} symb_to_PartIR g{*}symb_to_PartIR g | scomp g f => (symbPF_deriv g[o]symb_to_PartIR f){*} symbPF_deriv f end.
imports: CoRN.ftc.MoreFunSeries CoRN.ftc.Composition CoRN.tactics.DiffTactics2