Zulip Chat Archive

Stream: general

Topic: div_le_iff


Patrick Massot (Jun 06 2019 at 08:20):

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 (Jun 06 2019 at 08:51):

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 (Jun 06 2019 at 08:52):

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

Rob Lewis (Jun 06 2019 at 12:01):

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.


Last updated: Aug 03 2023 at 10:10 UTC