proposition: Lemma Derivative_I_const : forall c : IR, Derivative_I Hab' [-C-]c [-C-][0].
proof: Proof. intros. apply Derivative_I_char. Included. Included. intros e He. exists OneR. apply pos_one. intros. simpl in |- *. apply leEq_wdl with ZeroR. astepl (ZeroR[*][0]); apply mult_resp_leEq_both; try apply leEq_reflexive. apply less_leEq; assumption. apply AbsIR_nonneg. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply AbsIRz_isz. apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.Derivative