chore(algebra/order/sub): Generalize lemmas (#15497)

Generalize many lemmas from `canonically_ordered_add_monoid` to `has_exists_add_of_le`, and a few other generalizations.

### New lemmas
* `mul_le_cancellable_one`/`add_le_cancellable_zero`
* `tsub_add_le_right_comm`
* `add_tsub_add_le_tsub_left`
* `add_tsub_add_le_tsub_right`

src/algebra/big_operators/multiset.lean

@@ -153,10 +153,7 @@ lemma dvd_prod : a ∈ s → a ∣ s.prod :=
 quotient.induction_on s (λ l a h, by simpa using list.dvd_prod h) a
 
 lemma prod_dvd_prod_of_le (h : s ≤ t) : s.prod ∣ t.prod :=
-begin
-  obtain ⟨z, rfl⟩ := multiset.le_iff_exists_add.1 h,
-  simp only [prod_add, dvd_mul_right],
-end
+by { obtain ⟨z, rfl⟩ := exists_add_of_le h, simp only [prod_add, dvd_mul_right] }
 
 end comm_monoid
 

src/algebra/order/monoid_lemmas.lean

@@ -1068,6 +1068,9 @@ lemma contravariant.mul_le_cancellable [has_mul α] [has_le α] [contravariant_c
   {a : α} : mul_le_cancellable a :=
 λ b c, le_of_mul_le_mul_left'
 
+@[to_additive] lemma mul_le_cancellable_one [monoid α] [has_le α] : mul_le_cancellable (1 : α) :=
+λ a b, by simpa only [one_mul] using id
+
 namespace mul_le_cancellable
 
 @[to_additive]

src/algebra/order/ring.lean

@@ -1514,7 +1514,7 @@ instance to_no_zero_divisors : no_zero_divisors α :=
 instance to_covariant_mul_le : covariant_class α α (*) (≤) :=
 begin
   refine ⟨λ a b c h, _⟩,
-  rcases le_iff_exists_add.1 h with ⟨c, rfl⟩,
+  rcases exists_add_of_le h with ⟨c, rfl⟩,
   rw mul_add,
   apply self_le_add_right
 end