have hb8 := val_b8_of_val_ai evr e h1 h2 h3 h4 h6
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
⊢ v evr.valtn (discr e) ≥ 12
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ v evr.valtn (discr e) ≥ 12