Commit 2021-01-27 16:19 1011601d

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. I did not know where to put these lemmas. Please let me know your opinion.
5. Extract 4 auxiliary lemmas that are not specific to continued fraction but more generally about rational numbers, integers, and natural numbers starting from here. Again, I did not know where to put these. Please let me know your opinion.