mathlib3

2a21a861 - refactor(algebra/order/ring): turn `sq_le_sq` into an `iff` (#14511)

refactor(algebra/order/ring): turn `sq_le_sq` into an `iff` (#14511) * `sq_le_sq` and `sq_lt_sq` are now `iff` lemmas; * drop `abs_le_abs_of_sq_le_sq` and `abs_lt_abs_of_sq_lt_sq`.