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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : m ≤ v nav a
hb : n ≤ v nav b
⊢ m + n ≤ v nav (a * b)
Tactic:
rw [nav.v_mul_eq_add_v]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : m ≤ v nav a
hb : n ≤ v nav b
⊢ m + n ≤ v nav a + v nav b

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : m ≤ v nav a
hb : n ≤ v nav b
⊢ m + n ≤ v nav a + v nav b
Tactic:
exact add_le_add ha hb
State after:
no goals