rfl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) = ENatValRing.sub_val evr (One.one + 3) (e.a1 * e.a3 + 2 * e.a4)
no goals