Hello Everyone 
,
I could appreciate some advice from more seasoned users as I work on a project that includes formalising multiple mathematical conclusions using Coq proof assistance.
My primary area of expertise is mathematics, so even though I have a bit experience with Coq, I’m currently learning about its best practices and more sophisticated capabilities.
I am concentrating on theorems from actual analysis that deal with sequences and series.
Here are a few areas where I’m having trouble:
Formalising Convergence and Limits: I’m attempting to codify the idea of a limit for a real number series. Although I can grasp the mathematical definition, I’m having trouble translating it into Coq. I would be grateful for any guidance on managing ε-δ arguments in The coq and determining limits.
Interacting using Real Numbers: I am finding that several operations and proofs are tedious when working with real numbers, thus I am utilising the R type from the Coq standard library. Exist any hints or resources that make utilising actual values in Coq easier? 
Inductive Illustrations and Infinite Sequence: I have to demonstrate the convergence and sum of an infinite series, among other things. I’m still not quite sure how inductive proofs work in Coq, especially when it comes to sequences.
How can I apply induction techniques in Coq successfully for these kinds of proofs?
General Best Practices: It would be very beneficial to receive any general guidance on the best ways to organise proofs, handle hypotheses, and steer clear of typical mistakes.
I checked this: https://mathoverflow.net/questions/59520/how-true-are-tableau-theorems-proved-by-coq
If you know of any helpful tutorials or resources that would be appropriate for someone in my situation, please let me know.
Thank you 
in advance for your suggestions.