feat(algebra/ordered_monoid_lemmas + fixes): consistent use of `covar…

…iant` and `contravariant` in `ordered_monoid_lemmas` (#7876)

This PR breaks off a part of PR #7645.  Here, I start using more consistently `covariant_class` and `contravariant_class` in the file `algebra/ordered_monoid_lemmas`.

This PR is simply intended as a stepping stone to merging the bigger one (#7645) and receiving "personalized comments on it!

Summary of changes:
--
New lemmas
* `@[to_additive add_nonneg] lemma one_le_mul_right`
* `@[to_additive] lemma le_mul_of_le_of_le_one`
* `@[to_additive] lemma mul_lt_mul_of_lt_of_lt`
* `@[to_additive] lemma left.mul_lt_one_of_lt_of_lt_one`
* `@[to_additive] lemma right.mul_lt_one_of_lt_of_lt_one`
* `@[to_additive] lemma left.mul_lt_one_of_lt_of_lt_one`
* `@[to_additive] lemma right.mul_lt_one_of_lt_of_lt_one`
* `@[to_additive right.add_nonneg] lemma right.one_le_mul`
* `@[to_additive right.pos_add] lemma right.one_lt_mul`

--
Lemmas that have merged with their unprimed versions due to diminished typeclass assumptions
* `@[to_additive] lemma lt_mul_of_one_le_of_lt'`
* `@[to_additive] lemma lt_mul_of_one_lt_of_lt'`
* `@[to_additive] lemma mul_le_of_le_of_le_one'`
* `@[to_additive] lemma mul_le_of_le_one_of_le'`
* `@[to_additive] lemma mul_lt_of_lt_of_le_one'`
* `@[to_additive] lemma mul_lt_of_lt_of_lt_one'`
* `@[to_additive] lemma mul_lt_of_lt_one_of_lt'`
* the three lemmas
* * `@[to_additive] lemma mul_lt_of_le_one_of_lt'`,
* * `mul_lt_one_of_le_one_of_lt_one`,
* * `mul_lt_one_of_le_one_of_lt_one'`
all merged into `mul_lt_of_le_one_of_lt`

--
Lemma `@[to_additive] lemma mul_lt_one` broke into
* `@[to_additive] lemma left.mul_lt_one`
* `@[to_additive] lemma right.mul_lt_one`

depending on typeclass assumptions

--
Lemmas that became a direct application of another lemma
* `@[to_additive] lemma mul_lt_one_of_lt_one_of_le_one` and `mul_lt_one_of_lt_one_of_le_one'` are applications of `mul_lt_of_lt_of_le_one`
* `@[to_additive] lemma mul_lt_one'` is an application of `mul_lt_of_lt_of_lt_one`

--
Lemma `@[to_additive] lemma mul_eq_one_iff_eq_one_of_one_le` changed name to `mul_eq_one_iff_eq_one_of_one_le`.
The multiplicative version is never used.
The additive version, `add_eq_zero_iff_eq_zero_of_nonneg` is used: I changed the occurrences in favour of the shorter name.

--
Lemma `@[to_additive add_nonpos] lemma mul_le_one'` continues as
```lean
alias mul_le_of_le_of_le_one ← mul_le_one'
attribute [to_additive add_nonpos] mul_le_one'
```

<!--
Name changes:

* lemma `mul_le_of_le_one_of_le'` became `mul_le_of_le_one_of_le`;
* lemma `lt_mul_of_one_le_of_lt'` became `lt_mul_of_one_le_of_lt`;
* lemma `add_eq_zero_iff_eq_zero_of_nonneg` became `add_eq_zero_iff'`.

(Really, the lemmas above are the ones that were used outside of the PR: the two `mul` ones have a corresponding `to_additive` version and the `add` one is the `to_additive` version of `mul_eq_one_iff_eq_one_of_one_le`.)
-->

src/algebra/big_operators/order.lean

@@ -244,7 +244,7 @@ by classical;
 calc ∏ x in s, f x = (∏ x in s.filter (λ x, f x = 1), f x) * ∏ x in s.filter (λ x, f x ≠ 1), f x :
     by rw [← prod_union, filter_union_filter_neg_eq];
        exact disjoint_filter.2 (assume _ _ h n_h, n_h h)
-  ... ≤ (∏ x in t, f x) : mul_le_of_le_one_of_le'
+  ... ≤ (∏ x in t, f x) : mul_le_of_le_one_of_le
       (prod_le_one' $ by simp only [mem_filter, and_imp]; exact λ _ _, le_of_eq)
       (prod_le_prod_of_subset' $ by simpa only [subset_iff, mem_filter, and_imp])
 

src/algebra/ordered_monoid.lean

@@ -135,7 +135,7 @@ lemma top_add (a : α) : ⊤ + a = ⊤ := linear_ordered_add_comm_monoid_with_to
 
 @[simp]
 lemma add_top (a : α) : a + ⊤ = ⊤ :=
-by rw [add_comm, top_add]
+trans (add_comm _ _) (top_add _)
 
 end linear_ordered_add_comm_monoid_with_top
 
@@ -835,6 +835,11 @@ instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
   ..order_dual.partial_order α,
   ..show comm_monoid α, by apply_instance }
 
+@[to_additive ordered_cancel_add_comm_monoid.to_contravariant_class]
+instance ordered_cancel_comm_monoid.to_contravariant_class [ordered_cancel_comm_monoid α] :
+  contravariant_class (order_dual α) (order_dual α) has_mul.mul has_le.le :=
+{ elim := λ a b c bc, (ordered_cancel_comm_monoid.le_of_mul_le_mul_left a c b (dual_le.mp bc)) }
+
 @[to_additive]
 instance [ordered_cancel_comm_monoid α] : ordered_cancel_comm_monoid (order_dual α) :=
 { le_of_mul_le_mul_left := λ a b c : α, le_of_mul_le_mul_left',