proposition: Lemma derive_pt_const : forall x v p, derive_pt (fct_cte v) x p = 0.
proof: Proof. intros x v p ; transitivity (derive_pt (fct_cte v) x (derivable_pt_const v x)). apply derive_pt_ext ; reflexivity. apply derive_pt_const. Qed.
imports: Rbase Rpower Ranalysis Lra Rfunctions Rfunction_def Rextensionality MyRIneq MyR_dist Rtopology Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity