inequality following from a stronger inequality

Stream: new members

[Damiano Testa]

Dear All,

I use the lemma below to shorten a proof, as is usually the case with lemmas! :wink:

Since I would like the final lemma to go into mathlib, I would like the lemma below to also go. Should this lemma go to some general file (feel free to suggest which!) or should it stay close to the intended application?

Here is a wordy description of the lemma: to prove that the inequality 1 ≤ a * b holds, it suffices to prove

• the inequality 1 ≤ a; and
• if 1 < b, then to provide a c ≤ b satisfying 1 ≤ a * c.
  This lemma is mostly useful if c already appears in the context, especially in situations when the terms a and b are complicated.

import algebra.ordered_ring

lemma one_le_mul_of_le_and_of_lt {R : Type*} [linear_ordered_semiring R] {a b : R} (c : R)
  (ha   : 1 ≤ a)
  (key  : b < 1 → 1 ≤ a * c ∧ c ≤ b) :
  1 ≤ a * b :=
begin
  by_cases A : b < 1,
  { exact (key A).1.trans ((mul_le_mul_left (zero_lt_one.trans_le ha)).mpr (key A).2) },
  { rw ← mul_one (1 : R),
    exact mul_le_mul ha (not_lt.mp A) zero_le_one (zero_le_one.trans ha) }
end

[Floris van Doorn]

I see no value having this lemma in a general file. This lemma will probably not come up again in this exact form, and even if it does, it is unlikely that the user that wants this lemma will find it.

If you use this in only one theorem, I would not even separate this out as a separate lemma, but just prove it as a have, like this.

[Damiano Testa]

Floris, thank you so much, also for the commented pointer!