Commit 2020-08-10 19:28 9e039956

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.