Theorem: test_mul_both (Ray/Tactic/BoundTests.lean)

State before:
a b c x y : ℝ
z : ℂ
n : ℕ
bp : b ≥ 0
xp : x ≥ 0
ab : a ≤ b
xy : x ≤ y
⊢ a * x ≤ b * y
Tactic:
bound
State after:
no goals