rw [Model.rst_b2]
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
⊢ v valp (Model.b2 (Model.rst_iso r s t e.toModel)) ≥ 1
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
⊢ v valp (Model.b2 e.toModel + 12 * r) ≥ 1