apply val_add_ge_of_ge valp <;>
. simp
  elinarith
R : Type u
inst✝ : CommRing R
inst : IsDomain R
q : ℕ∞
p : R
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h3 : v valp e.a3 ≥ q
h4 : v valp e.a4 ≥ q + 1
⊢ v valp (Model.b4 e.toModel) ≥ q + 1
no goals