rw [(show (12 : R) = 2 * 6 by norm_num)]
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp 12 ≥ 1
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp (2 * 6) ≥ 1