Is there a mul_lt_iff_lt_div

Stream: Is there code for X?

[Ben]

Don't completely understand ordering on the reals yet, just need for a bigger example. Is there a proof of the following in mathlib:

lemma mul_lt_iff_lt_div (a b c d: real) (h1: a < d) (h2: c > 0) (h3: d > 0)
  : a * b < c ↔ b < c / d := by sorry

Is it even true :joy: , am I missing any other bounds on the inputs?

[Michael Stoll]

Set a = -1, b = 1, c = 1, d = 2...

[Ben]

Hmm yes, what about adding the constraints that a > 0 and b > 0..?

[Andrew Yang]

I don't see how the iff can hold when $a \ne d$? What if $c = ab + \varepsilon$ and $d$ is arbitrarily large?

[Michael Stoll]

The right hand side is equivalent to b * d < c, so for an iff you need a = d.

[Ben]

Hmm yes. I am getting mixed up with all the variables, here is a less abstract representation of what I am need a proof

example (x y c L: real) (h1: c > 0) (h2: |x| < L) : |x| * |y| < c → |y| < c / L := by sorry

Is there any contradictory cases here...?

[Patrick Johnson]

A counterexample is x = 1, y = 1, c = 2, L = 2

example : ¬Π (x y c L: real) (h1: c > 0) (h2: |x| < L), |x| * |y| < c → |y| < c / L :=
by { push_neg, use [1, 1, 2, 2], norm_num }

[Ben]

Hmm need to have another think, I think I am trying to prove something that only works forwards, backwards...

[Ruben Van de Velde]

It happens surprisingly often that a lemma is hard to formalise because it's false :sweat_smile: