checkpoint commit. more progress on LUB prop
Finish proving that the square root of 2 is a real number