nat.sqrt and pow 2

Stream: maths

[Patrick Stevens]

Would anyone object if I went through data.nat.sqrt and added versions of all the lemmas to talk about n ^ 2 instead of n * n?

[Mario Carneiro]

go for it