exact (pi_scaling_of_b4 evr e h1 h3 h4).symm
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 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 + 2 * ENatValRing.sub_val evr 4 e.a4 =
    ENatValRing.sub_val evr 4 (e.a1 * e.a3 + 2 * e.a4)
no goals