have h4' : valp e.b4 ≥ q + 1 := v_b4_of_v_a1_a3_a4 valp e h1 h3 h4
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3