proposition: Lemma derivable_pt_lim_const : forall a x:R, derivable_pt_lim (fct_cte a) x 0.
proof: Proof. intros; unfold fct_cte, derivable_pt_lim. intros; exists (mkposreal 1 Rlt_0_1); intros; unfold Rminus; rewrite Rplus_opp_r; unfold Rdiv; rewrite Rmult_0_l; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv