mathlib documentation

tactic.monotonicity.lemmas

theorem mul_mono_nonneg {α : Type u_1} {x y z : α} [ordered_semiring α] :
0 zx yx * z y * z

theorem lt_of_mul_lt_mul_neg_right {α : Type u_1} {a b c : α} [linear_ordered_ring α] :
a * c < b * cc 0b < a

theorem mul_mono_nonpos {α : Type u_1} {x y z : α} [linear_ordered_ring α] :
z 0y xx * z y * z

theorem nat.sub_mono_left_strict {x y z : } :
z xx < yx - z < y - z

theorem nat.sub_mono_right_strict {x y z : } :
x zy < xz - x < z - y