[GOAL]
α : Type u
inst✝³ : OrderedCancelCommMonoid α
β : Type u_1
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝ : OrderedCommMonoid β := orderedCommMonoid f hf one mul npow
a b c : β
bc : f (a * b) ≤ f (a * c)
⊢ f a * f b ≤ f a * f c
[PROOFSTEP]
rwa [← mul, ← mul]
