. rfl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) = ENatValRing.sub_val evr (3 + 3) (e.a3 * e.a3 + 4 * e.a6)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)