proposition: Lemma continuity_minus : forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 - f2).
proof: Proof. unfold continuity ; intros ; apply continuity_pt_minus ; intuition. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def