chore(*): use `sq` as convention for "squared" (#7368)
This PR establishes `sq x` as the notation for `x ^ 2`. See [this Zulip conversation](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/sqr.20vs.20sq.20vs.20pow_two/near/224972795).
A breakdown of the refactor:
- All instances of `square` and `sqr` are changed to `sq` (except where `square` means something other than "to the second power")
- All instances of `pow_two` are changed to `sq`, though many are kept are aliases
- All instances of `sum_of_two_squares` are changed to `sq_add_sq`
n.b. I did NOT alter any instances of:
- `squarefree`
- `sum_of_four_squares`
- `fpow_two` or `rpow_two`
<!-- The text above the `
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
