fact: Fixpoint Derivative_I_n (n : nat) (F Fn : PartIR) {struct n} : CProp := match n with | O => Feq I F Fn | S p => {f' : CSetoid_fun (subset (Compact Hab)) IR | Derivative_I Hab' F (PartInt f') | Derivative_I_n p (PartInt f') Fn} end.
imports: CoRN.ftc.Differentiability