Theorem: Model.val_b8_of_val_ai (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
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
⊢ v evr.valtn (b8 e) ≥ 8
Tactic:
simp only [b8, sub_eq_add_neg]
State after:
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
⊢ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 + -(e.a4 * e.a4)) ≥ 8

State before:
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
⊢ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 + -(e.a4 * e.a4)) ≥ 8
Tactic:
apply val_add_ge_of_ge
State after:
case ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3)

case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))

State before:
case ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3)

case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))
Tactic:
. apply val_add_ge_of_ge
  . apply val_add_ge_of_ge
    . apply val_add_ge_of_ge
      . apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h1) h6
      . rw [val_neg]
        apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h3) h4
    . rw [mul_assoc]
      apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ h2 h6)
  . apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h2 h3) h3
State after:
case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))

State before:
case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))
Tactic:
. rw [val_neg]
  apply val_mul_ge_of_both_ge _ h4 h4
State after:
no goals

State before:
case ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3)
Tactic:
apply val_add_ge_of_ge
State after:
case ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)

case ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)

State before:
case ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)

case ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
Tactic:
. apply val_add_ge_of_ge
  . apply val_add_ge_of_ge
    . apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h1) h6
    . rw [val_neg]
      apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h3) h4
  . rw [mul_assoc]
    apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ h2 h6)
State after:
case ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)

State before:
case ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
Tactic:
. apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h2 h3) h3
State after:
no goals

State before:
case ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)
Tactic:
apply val_add_ge_of_ge
State after:
case ha.ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))

case ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (4 * e.a2 * e.a6)

State before:
case ha.ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))

case ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (4 * e.a2 * e.a6)
Tactic:
. apply val_add_ge_of_ge
  . apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h1) h6
  . rw [val_neg]
    apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h3) h4
State after:
case ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (4 * e.a2 * e.a6)

State before:
case ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (4 * e.a2 * e.a6)
Tactic:
. rw [mul_assoc]
  apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ h2 h6)
State after:
no goals

State before:
case ha.ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))
Tactic:
apply val_add_ge_of_ge
State after:
case ha.ha.ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)

case ha.ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))

State before:
case ha.ha.ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)

case ha.ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
Tactic:
. apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h1) h6
State after:
case ha.ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))

State before:
case ha.ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
Tactic:
. rw [val_neg]
  apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h3) h4
State after:
no goals

State before:
case ha.ha.ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
Tactic:
apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h1) h6
State after:
no goals

State before:
case ha.ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
Tactic:
rw [val_neg]
State after:
case ha.ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)

State before:
case ha.ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
Tactic:
apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h3) h4
State after:
no goals

State before:
case ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (4 * e.a2 * e.a6)
Tactic:
rw [mul_assoc]
State after:
case ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (4 * (e.a2 * e.a6))

State before:
case ha.ha.hb
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
⊢ 8 ≤ v evr.valtn (4 * (e.a2 * e.a6))
Tactic:
apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ h2 h6)
State after:
no goals

State before:
case ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
Tactic:
apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h2 h3) h3
State after:
no goals

State before:
case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))
Tactic:
rw [val_neg]
State after:
case hb
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
⊢ 8 ≤ v evr.valtn (e.a4 * e.a4)

State before:
case hb
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
⊢ 8 ≤ v evr.valtn (e.a4 * e.a4)
Tactic:
apply val_mul_ge_of_both_ge _ h4 h4
State after:
no goals