proposition: Lemma continuity_pt_const : forall f (x0:R), constant f -> continuity_pt f x0.
proof: Proof. unfold constant, continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; intros; exists 1; split; [ apply Rlt_0_1 | intros; generalize (H x x0); intro; rewrite H2; simpl; rewrite Rdist_eq; assumption ]. Qed.
imports: Rbase Rfunctions Rlimit Rderiv