proposition: Lemma continuity_scal : forall f a, continuity f -> continuity (mult_real_fct a f).
proof: Proof. unfold continuity ; intros ; apply continuity_pt_scal ; intuition. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def