Theorem: ENatValRing.val_sub_val_le (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
h : ↑m ≤ v evr.valtn x
⊢ v evr.valtn (sub_val evr n x) ≥ ↑m - ↑n
Tactic:
sorry
State after:
no goals