In other words, how to prove that every Cauchy sequence is convergent.

Is there some good proof of it in Coq? In standard library or somewhere else...

Because I'm having problems translating the proof of book to Coq. :(

False alert, I managed to do it. :)

Lessness has marked this topic as resolved.

given that the Stdlib now has Cauchy sequences, I think this fact must be in Stdlib as well...

Last updated: Feb 04 2023 at 22:29 UTC