sqrt 4 = 2 by Def2, Lm4;