a * b < a * c and b < c implies 0 < a

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Do we have sth like this?

import Mathlib

theorem pos_of_mul_lt_lt {R : Type*} [Semiring R] [LinearOrder R] {a b c : R} [ExistsAddOfLE R]
    [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R]
    (h : a * b < a * c) (hbc : b < c) :
    0 < a := by
  rcases lt_trichotomy 0 a with (ha | ha | ha)
  · exact ha
  · subst ha; simp_all
  · grind [mul_lt_mul_of_neg_left hbc ha]

[Ruben Van de Velde]

No, I can't find anything like it

[Miyahara Kō]

I couldn't find in Loogle, too.
Result: ?a * ?b < ?a * ?c
Result: ?a * ?c < ?b * ?c

[Yury G. Kudryashov]

• It looks like we don't have this.
• I think that you can replace hbc with a non-strict inequality, because if b = c, then a * b = a * c, so this case is in fact impossible.

[Yury G. Kudryashov]

I think, the closest thing we have is docs#pos_of_mul_pos_right and nearby lemmas.

[Yongxi Lin (Aaron)]

#35302