chore(algebra/ordered_field): cleanup (#3723)
* drop `mul_zero_lt_mul_inv_of_pos` and `mul_zero_lt_mul_inv_of_neg`;
* add `iff` lemmas `one_div_pos/neg/nonneg/nonpos` replacing old
implications;
* some lemmas now assume `≤` instead of `<`;
* rename `mul_lt_of_gt_div_of_neg` to `mul_lt_of_neg_of_div_lt`
replacing `>` by `<`.
* add `mul_sub_mul_div_mul_neg_iff` and `mul_sub_mul_div_mul_nonpos_iff`,
generate implications using `alias`;
* drop `div_pos_of_pos_of_pos` (use `div_pos`) and
`div_nonneg_of_nonneg_of_pos` (use `div_nonneg`);
* replace `div_nonpos_of_nonpos_of_pos` with
`div_nonpos_of_nonpos_of_nonneg`;
* replace `div_nonpos_of_nonneg_of_neg` with
`div_nonpos_of_nonneg_of_nonpos`;
* replace `div_mul_le_div_mul_of_div_le_div_pos` and
`div_mul_le_div_mul_of_div_le_div_pos'` with
`div_mul_le_div_mul_of_div_le_div_nonneg`; I failed to find
in the history why we had two equivalent lemmas.
* merge `le_mul_of_ge_one_right` and `le_mul_of_one_le_right'` into
`le_mul_of_one_le_right`, rename old `le_mul_of_one_le_right` to
`le_mul_of_one_le_right'`;
* ditto with `le_mul_of_ge_one_left`, `le_mul_of_one_le_left`, and
`le_mul_of_one_le_left'`;
* ditto with `lt_mul_of_gt_one_right`, `lt_mul_of_one_lt_right`, and
`lt_mul_of_one_lt_right'`;
* rename `div_lt_of_mul_lt_of_pos` to `div_lt_of_pos_of_lt_mul`;
* rename `div_lt_of_mul_gt_of_neg` to `div_lt_of_neg_of_mul_lt`;
* rename `mul_le_of_div_le_of_neg` to `mul_le_of_neg_of_div_le`;
* rename `div_le_of_mul_le_of_neg` to `div_le_of_neg_of_mul_le`;
* rename `div_lt_div_of_lt_of_pos` to `div_lt_div_of_pos_of_lt`, swap
arguments;
* rename `div_le_div_of_le_of_pos` to `div_le_div_of_pos_of_le`, swap
arguments;
* rename `div_lt_div_of_lt_of_neg` to `div_lt_div_of_neg_of_lt`, swap
arguments;
* rename `div_le_div_of_le_of_neg` to `div_le_div_of_neg_of_le`, swap
arguments;
* rename `one_div_lt_one_div_of_lt_of_neg` to
`one_div_lt_one_div_of_neg_of_lt`;
* rename `one_div_le_one_div_of_le_of_neg` to
`one_div_le_one_div_of_neg_of_le`;
* rename `le_of_one_div_le_one_div_of_neg` to
`le_of_neg_of_one_div_le_one_div`;
* rename `lt_of_one_div_lt_one_div_of_neg` to
`lt_of_neg_of_one_div_lt_one_div`;
* rename `one_div_le_of_one_div_le_of_pos` to
`one_div_le_of_pos_of_one_div_le`;
* rename `one_div_le_of_one_div_le_of_neg` to
`one_div_le_of_neg_of_one_div_le`.
