intro x y h
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ Function.Injective fun x => x + v nav p
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x y : ℕ∞
h : (fun x => x + v nav p) x = (fun x => x + v nav p) y
⊢ x = y