neg_of_neg_of_div_pos

Stream: mathlib4

[Bjørn Kjos-Hanssen]

Maybe this is a missing lemma in Mathlib? Or is there a truly quick way to get it?

lemma neg_of_neg_of_div_pos (a b : ℝ) (h : 0 < a/b) (h₁ : b < 0) : a < 0 := by
    contrapose h
    rw [not_lt]
    rw [not_lt] at h
    exact div_nonpos_of_nonneg_of_nonpos h (by linarith)

lemma neg_of_neg_of_div_pos (a b : ℝ) (h : 0 < a/b) (h₁ : b < 0) : a < 0 :=
    Left.neg_pos_iff.mp <| (div_pos_iff_of_pos_right <|Left.neg_pos_iff.mpr h₁).mp
        <|(neg_div_neg_eq a b) ▸ h

[Yaël Dillies]

Using the corresponding mul lemma + docs#inv_pos should be faster

[Yaël Dillies]

@bjoernkjoshanssen, här: #18260

[Bjørn Kjos-Hanssen]

Takk for den!