inequality involving `/2`

Stream: Is there code for X?

[Scott Morrison]

I am finding this unusually painful. Can anyone point me in the right direction:

import data.real.basic
example (a b : ℝ) : a/2 + b < a ↔ b < a/2 := sorry

[Scott Morrison]

Ahhh:

example (a b : ℝ) : a/2 + b < a ↔ b < a/2 := by fsplit; { intro, linarith, }

[Scott Morrison]

I still wouldn't mind seeing a "by hand" proof.

[Damiano Testa]

Does this count as "by hand"?

example (a b : ℝ) : a/2 + b < a ↔ b < a/2 :=
by rw [← lt_sub_iff_add_lt', sub_half]

Since those are chains of iff's, you may be able to avoid the rw.

[Damiano Testa]

Scott, I am not really sure that I can help you with using Lean, but I had seen halfs before somewhere else and I guessed that a lemma to move the a / 2 summand to the right would focus on the subafter the fact, so I searched for lt_sub... instead of add_lt....

I do feel silly making these comments to you, but, putting them in writing, helps clear out something in my mind as well!

[Scott Morrison]

Ah! It was lt_sub_iff_add_lt' that I failed to find. Thank you.