exact general x
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
general : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x
no goals