feat(data/nat/sqrt0): Add sqrt0
Throughout mathlib, there are several types `α` for which a notion of `sqrt` has been defined.
For instance, `nat.sqrt`, `int.sqrt`, `nnreal.sqrt`, and `real.sqrt`. In most cases, `sqrt x` is
defined as the greatest `y ∈ α` such that `y * y ≤ x` or `0` if no such `y` exists.
But this definition has some limits. For example, it's not true for `rat.sqrt`. (Indeed, the
squares are dense in the positive reals, so such a definintion can't work for the rationals.)
The following definition offers a different take on how to handle the "undefined" aspect of
`sqrt`. Specifically, in `ℕ`, if `¬is_square x`, then we'll define `sqrt0 x = 0`. Otherwise, we'll
define `sqrt0 x` as the (unique) `y` such that `x = y * y`.
NOTE: This is to be used for my ongoing work to prove asymptotics for
squarefree integers where it is used in a sum swap.
NOTE: This is currently blocked by #12992 (for decidability) and #13268
(a refactor of some dependencies)
