apply val_mul_ge_of_left_ge
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp (3 * 4) ≥ 1
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp 3