proposition: Lemma continuity_in_const : forall D c, continuity_in D (fun _ => c).
proof: Proof. intros ; exists 1 ; split ; [lra |] ; intros ; rewrite R_dist_eq ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics