proposition: Lemma limit_opp : forall (f:C -> C) (D:C -> Prop) (l x0:C), limit1_in f D l x0 -> limit1_in (fun x:C => - f x) D (- l) x0.
proof: Proof. unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; split with x; split; auto; intros; generalize (H1 x1 H2); clear H1; intro; unfold C_dist in |- *; unfold Cminus in |- *; rewrite (Copp_involutive l); rewrite (Cadd_comm (- f x1) l); fold (l - f x1) in |- *; fold (C_dist l (f x1)) in |- *; rewrite C_dist_sym; assumption. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions