proposition: Lemma derivable_pt_lim_in_const: forall D k x, derivable_pt_lim_in D (fun _ => k) x 0.
proof: Proof. intros D k x eps eps_pos ; exists 1 ; intros ; split. lra. intros ; simpl ; unfold R_dist, growth_rate, Rminus, Rdiv ; rewrite Rplus_opp_r, Rmult_0_l, Rplus_opp_r, Rabs_R0 ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics