proposition: Lemma Diffble_I_const : forall c : IR, Diffble_I Hab' [-C-]c.
proof: Proof. intros. exists (IConst (Hab:=Hab) [0]). apply Derivative_I_wdr with ( [-C-][0]:PartIR). apply part_int_const. Deriv. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps