Commit 2020-06-14 09:10 2cd329fe

feat(algebra/continued_fractions): add correctness of terminating computations (#2911)

What

Add correctness lemmas for terminating computations of continued fractions

Why

To show that the continued fractions algorithm is computing the right thing in case of termination. For non-terminating sequences, lemmas about the limit will be added in a later PR.

How

1. Show that the value to be approximated can always be obtained by adding the corresponding, remaining fractional part stored in int_fract_pair.stream.
2. Use this to derive that once the fractional part becomes 0 (and hence the continued fraction terminates), we have exactly computed the value.