. exact val_mul_ge_of_right_ge evr.valtn (val_pow_ge_of_ge evr.valtn 3 hb4)
case hx.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (8 * b4 e ^ 3)
no goals