fact: Fixpoint Diffble_I_n (n : nat) (F : PartIR) {struct n} : CProp := match n with | O => included I (Dom F) | S p => {H : Diffble_I Hab' F | Diffble_I_n p (PartInt (ProjT1 H))} end.
imports: CoRN.ftc.Differentiability