exact val_mul_ge_of_left_ge valp h_p
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ 1 ≤ v valp (12 * r)
no goals