mathlib

8fd37661 - Eliminate `finish` from `exists_succ_nth_stream_of_fr_zero`