mathlib documentation

theorem mul_mono_nonneg {α : Type u_1} {x y z : α} [ordered_semiring α] (h' : 0 ≤ z) (h : x ≤ y) :

theorem lt_of_mul_lt_mul_neg_right {α : Type u_1} {a b c : α} [linear_ordered_ring α] (h : a * c < b * c) (hc : c ≤ 0) :

theorem mul_mono_nonpos {α : Type u_1} {x y z : α} [linear_ordered_ring α] (h' : z ≤ 0) (h : y ≤ x) :

theorem nat.sub_mono_left_strict {x y z : ℕ} (h' : z ≤ x) (h : x < y) :

theorem nat.sub_mono_right_strict {x y z : ℕ} (h' : x ≤ z) (h : y < x) :