:: Introduction to {D}iophantine Approximation :: by Yasushige Watase :: :: Received April 19, 2015 :: Copyright (c) 2015-2016 Association of Mizar Users
:: Approximation an irrational by its simple continued fraction
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Proof of an existance of a solution of|. x*a -y .| < 1/t x < t
:: Dirichlet's argument
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::