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