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