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 <39661b8dc3ffe34e47f61e03ce7eb76906251f50@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib