proposition: Lemma Lim_recip : forall seq seq_ seq__, Lim (Build_CauchySeq _ _ (Cauchy_recip seq seq_ seq__)) [=] ([1][/] _[//]seq__).
proof: Proof. intros. apply eq_symmetric_unfolded; apply Limits_unique. simpl in |- *; apply Cauchy_Lim_recip. apply Cauchy_complete. Qed.
imports: CoRN.reals.OddPolyRootIR