Theorem: SurjVal.val_mul_ge_right (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (a * b)
Tactic:
rw [mul_comm]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (b * a)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
⊢ v nav b ≤ v nav (b * a)
Tactic:
exact val_mul_ge_left nav b a
State after:
no goals