div_le_iff

Stream: general

[Patrick Massot]

Are library_search and I blind or is

lemma div_le_div_iff {α : Type*} [linear_ordered_field α] {b d : α} (hd : 0 < d) (hb : 0 < b) (a c : α) :
  a/b ≤ c/d ↔ d*a ≤ b*c :=
by rw [div_le_iff' hb, ← mul_div_assoc, le_div_iff' hd]

missing from https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ordered_field.lean?

[Patrick Massot]

What about the following one?

lemma sub_le_sub_iff {α : Type*} [ordered_comm_group α] (a b c d : α) :
a - b ≤ c - d ↔ a + d ≤ b + c :=
by rw [sub_le, ← sub_add, show a - c + d = a + d - c, by abel, sub_le_iff_le_add]

Why is linarith failing here?

[Patrick Massot]

at least in the case of real numbers, split ; intros ; linarith succeeds.

[Rob Lewis]

linarith assumes some algebraic structure that may not be strictly necessary, because it uses ring for the verification step. It will work if alpha is a linear_ordered_comm_ring.