proposition: Lemma limit_free : forall (f:C -> C) (D:C -> Prop) (x x0:C), limit1_in (fun h:C => f x) D (f x) x0.
proof: Proof. unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros; split with eps; split; auto; intros; elim (C_dist_refl (f x) (f x)); intros a b; rewrite (b (refl_equal (f x))); unfold Rgt in H; assumption. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions