exact val_add_ge_of_ge evr.valtn (val_add_ge_of_ge evr.valtn h116 h134) h26
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ((fun x x_1 => x + x_1) ↑2 ↑3) ↑3) ≤
    v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)
no goals