mathlib

1011601d - feat(algebra/continued_fractions): add termination iff rat lemmas (#4867)

feat(algebra/continued_fractions): add termination iff rat lemmas (#4867) ### What Show that the computation of a continued fraction terminates if and only if we compute the continued fraction of a rational number. ### How 1. Show that every intermediate operation involved in the computation of a continued fraction returns a value that has a rational counterpart. This then shows that a terminating continued fraction corresponds to a rational value. 2. Show that the operations involved in the computation of a continued fraction for rational numbers only return results that can be lifted to the result of the same operations done on an equal value in a suitable linear ordered, archimedean field with a floor function. 3. Show that the continued fraction of a rational number terminates. 4. Set up the needed coercions to express the results above starting from [here](https://github.com/leanprover-community/mathlib/compare/kappelmann_termination_iff_rat?expand=1#diff-1dbcf8473152b2d8fca024352bd899af37669b8af18792262c2d5d6f31148971R129). I did not know where to put these lemmas. Please let me know your opinion. 4. Extract 4 auxiliary lemmas that are not specific to continued fraction but more generally about rational numbers, integers, and natural numbers starting from [here](https://github.com/leanprover-community/mathlib/compare/kappelmann_termination_iff_rat?expand=1#diff-1dbcf8473152b2d8fca024352bd899af37669b8af18792262c2d5d6f31148971R28). Again, I did not know where to put these. Please let me know your opinion. Co-authored-by: Kevin Kappelmann <kappelmann@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>