proposition: Lemma derivable_pt_lim_const : forall a x, derivable_pt_lim (fct_cte a) x 0.
proof: Proof. intros; unfold fct_cte, derivable_pt_lim in |- *. intros; exists (mkposreal 1 Rlt_0_1); intros; unfold Cminus in |- *; rewrite Cadd_opp_r; unfold Cdiv in |- * ; rewrite Cmult_0_l; rewrite Cadd_opp_r; rewrite Cnorm_C0; assumption. Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv