mathlib3

c2c7afe9 - feat(data/nat/sqrt): add simple inequality lemmas and "no middle square" (#5155)

feat(data/nat/sqrt): add simple inequality lemmas and "no middle square" (#5155) The first two theorems are useful when one needs the biggest perfect square strictly less than a number, whereas `no_middle_square` can be used to easily prove that a given number is not a square. Co-authored-by: Adrián Doña Mateo <43966663+AdrianDoM@users.noreply.github.com>