[Merged by Bors] - feat(algebra/ordered_ring): add lemma

[adomani]

Add a lemma in algebra.ordered_ring proving the inequality a + (2 + b) ≤ a * (2 + b).

This is again part of the Liouville PR.

---

[eric-wieser]

I wonder if a more useful statement would be

Suggested change

	(a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
	(a2 : 2 ≤ a) (b0 : 2 ≤ b) : a + b ≤ a * b :=

It would certainly be easier to name (add_le_mul)

[eric-wieser]

Oh, maybe this is not true!

[adomani]

My intended application is indeed in the form that you suggest, for natural numbers. However, I was not able to prove the lemma that you stated in this level of generality.

[adomani]

I tried to put the version below somewhere else in this file but Lean says that it cannot produce the instance ordered_semiring α. I do not have examples of pathological canonically_ordered_comm_semirings, but it seems that they may not be ordered_semirings with added features.

Notice that the lemma below, also removing the @, works for ℕ, which is what I really care about.

lemma add_le_mul {α : Type*} [canonically_ordered_comm_semiring α] [nontrivial α]
  {a b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b :=
begin
  rcases (le_iff_exists_add).mp b2 with ⟨k, rfl⟩,
  exact @add_le_mul_two_add _ _ _ a k a2 k.zero_le
end

[adomani]

I am starting to get the impression that there is a missing instance, since a c_o_c_semiring is an ordered, commutative semiring with ... but the attempt below fails.

instance cosr {α : Type*} [canonically_ordered_comm_semiring α] : ordered_semiring α :=
by apply_instance

[adomani]

I am giving up trying to prove the result that I want in this generality, since I only care about it for the natural numbers.

Something appears to be weird around the left-cancellative property of addition, if I understand correctly the issue.

[eric-wieser]

I set this problem to the Xena Discord last night, and the consensus is that it may be false. @b-mehta was attempting to construct a pathological semiring to verify that.

[adomani]

Ok, I was going to ask on Zulip... do you want to do it yourself, or should I go ahead?

[eric-wieser]

Go ahead. I'll probably try to fix the typeclass issue you mentioned, but I don't intend to spend more time myself working out if the modified statement is true! We were able to prove 2*(a+b) ≤ 2*(a*b), but there's no way to cancel the two

[adomani]

Hmm, this 2*x ≤ 2*y implying x ≤ y may be the culprit. I wonder if there is some kind of 2-torsion that is allowed on canonically_ordered_... that may make the statement actually false.

[adomani]

Eric, I am tempted to leave this lemma where it is, as it is true and proved.

I am planning to include in a separate PR the lemma that Johan proved, on linear_ordered_semirings. Does this sound reasonable? Or should I remove the lemma in this PR and only prove the other one?

[b-mehta]

With #6034, the nontriviality assumption here is unnecessary.

[eric-wieser]

Worse than unnecessary, I think it will cause the lint build to fail.

[adomani]

If I managed to merge/leanproject up and push in the correct order, I should have removed the nontrivial assumption!

Thanks for picking this up!

[bryangingechen]

Thanks!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests