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