proposition: Lemma limit_minus : forall (f g:C -> C) (D:C -> Prop) (l l' x0:C), limit1_in f D l x0 -> limit1_in g D l' x0 -> limit1_in (fun x:C => f x - g x) D (l - l') x0.
proof: Proof. intros; unfold Cminus in |- *; generalize (limit_opp g D l' x0 H0); intro; exact (limit_plus f (fun x:C => - g x) D l (- l') x0 H H1). Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions