1 < sqrt 2 by Lm3, Th18;