simp [gaussian_val]
p : ℕ
a b : QuadRing ℤ 0 (-1)
⊢ gaussian_val p (a + b) ≥ min (gaussian_val p a) (gaussian_val p b)
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))