proposition: Theorem derivable_continuous_pt : forall f (x:R), derivable_pt f x -> continuity_pt f x.
proof: Proof. intros f x X. generalize (derivable_derive f x X); intro. elim H; intros l H1. cut (l = fct_cte l x). - intro. rewrite H0 in H1. generalize (derive_pt_D_in f (fct_cte l) x); intro. elim (H2 X); intros. generalize (H4 H1); intro. unfold continuity_pt. apply (cont_deriv f (fct_cte l) no_cond x H5). - unfold fct_cte; reflexivity. Qed.
imports: Rbase Rfunctions Rlimit Rderiv