rw [(show (12 : R) = 3 * 4 by norm_num)]
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp 12 ≥ 1
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp (3 * 4) ≥ 1