mathlib documentation

tactic.monotonicity.lemmas

theorem mul_mono_nonneg {α : Type u_1} {x y z : α} [ordered_semiring α] (h' : 0 z) (h : x y) :
x * z y * z
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) :
b < a
theorem mul_mono_nonpos {α : Type u_1} {x y z : α} [linear_ordered_ring α] (h' : z 0) (h : y x) :
x * z y * z
theorem nat.sub_mono_left_strict {x y z : } (h' : z x) (h : x < y) :
x - z < y - z
theorem nat.sub_mono_right_strict {x y z : } (h' : x z) (h : y < x) :
z - x < z - y