proposition: Lemma continuity_mult : forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 * f2).
proof: Proof. unfold continuity; intros; apply (continuity_pt_mult f1 f2 x (H x) (H0 x)). Qed.
imports: Rbase Rfunctions Rlimit Rderiv