mathlib

15b24348 - chore(data/nat/sqrt): Alternative phrasings of data.nat.sqrt lemmas (#7748)

chore(data/nat/sqrt): Alternative phrasings of data.nat.sqrt lemmas (#7748) Add versions of the `data.nat.sqrt` lemmas to talk about `n^2` where the current versions talk about `n * n`.