have h44 := val_mul_ge_of_both_ge evr.valtn h4 h4
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)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
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)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)