proposition: Lemma Diffble_I_id : Diffble_I Hab' FId.
proof: Proof. exists (IConst (Hab:=Hab) [1]). apply Derivative_I_wdr with ( [-C-][1]:PartIR). apply part_int_const. Deriv. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps