proposition: Lemma derivable_in_const : forall D k, derivable_in D (fun _ => k).
proof: Proof. intros D k x x_in ; eapply derivable_pt_in_const. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics