Theorem: QuadRing.gaussian_val_add_ge_min (ECTate/Algebra/QuadRing/Valuations.lean)

State before:
p : ℕ
a b : QuadRing ℤ 0 (-1)
⊢ gaussian_val p (a + b) ≥ min (gaussian_val p a) (gaussian_val p b)
Tactic:
simp [gaussian_val]
State after:
p : ℕ
a b : QuadRing ℤ 0 (-1)
⊢ ((Int.int_val p a.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∧
    ((Int.int_val p a.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b2 + b.b2)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b2 + b.b2))

State before:
p : ℕ
a b : QuadRing ℤ 0 (-1)
⊢ ((Int.int_val p a.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∧
    ((Int.int_val p a.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b2 + b.b2)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b2 + b.b2))
Tactic:
sorry
State after:
no goals