proposition: Lemma Cauchy_recip : forall seq seq_, Lim seq [#] ([0]:IR) -> Cauchy_prop (fun n => [1][/] seq n[//]seq_ n).
proof: Proof. intros seq Hn Hy. apply Cauchy_prop2_prop. exists ([1][/] _[//]Hy). apply Cauchy_Lim_recip. apply Cauchy_complete. Qed.
imports: CoRN.reals.OddPolyRootIR