proposition: Lemma continuity_pt_scal : forall f (a x0:R), continuity_pt f x0 -> continuity_pt (mult_real_fct a f) x0.
proof: Proof. unfold continuity_pt, mult_real_fct; unfold continue_in; intros; apply (limit_mul (fun x:R => a) f (D_x no_cond x0) a (f x0) x0). - unfold limit1_in; unfold limit_in; intros; exists 1; split. + apply Rlt_0_1. + intros; rewrite Rdist_eq; assumption. - assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv