exact val_mul_ge_of_both_ge evr.valtn h1 h3
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
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)
no goals