simp
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h3 : v valp e.a3 ≥ ↑q
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ 2 * ↑q ≤ v valp (4 * e.a6)
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h3 : v valp e.a3 ≥ ↑q
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ 2 * ↑q ≤ v valp 4 + v valp e.a6