fact: Fixpoint deriv_to_pfunct (r : deriv_function) : PartIR := match r with | hyp Hab' f f' H => f | hyp' Hab' f H => f | const c => [-C-]c | id => FId | rplus f g => deriv_to_pfunct f{+}deriv_to_pfunct g | rinv f => {--}(deriv_to_pfunct f) | rminus f g => deriv_to_pfunct f{-}deriv_to_pfunct g | rmult f g => deriv_to_pfunct f{*}deriv_to_pfunct g | rscalmult c f => c{**}deriv_to_pfunct f | rnth f n => deriv_to_pfunct f{^}n end.
imports: CoRN.ftc.Differentiability