how to solve this inequility for the general case?

Stream: mathlib4

[uri singer]

Linearity can't solve it for the general c > 0,

example (x y c: ℝ)  (h1: |x| < y / c )  (h2: c > 0) : c * |x| < y  := by
  linarith

The specific case does work

example (x y: ℝ)  (h1: |x| < y / 90)  : 90 * |x| < y  := by
  linarith

[Ira Fesefeldt]

Please include the import Mathlib in your example. That makes it easier to open.

If you include the theorem that transforms division into multiplication, linarith can take over the rest:

import Mathlib

example (x y c: ℝ)  (h1: |x| < y / c )  (h2: c > 0) : c * |x| < y  := by
  rw [lt_div_iff h2] at h1
  linarith

[Kevin Buzzard]

import Mathlib

example (x y c: ℝ)  (h1: |x| < y / c )  (h2: c > 0) : c * |x| < y  := by
  exact?

This is exactly the sort of lemma that one would expect to find in the library.