simp [gaussian_val]
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ gaussian_val p (a * b) = gaussian_val p a + gaussian_val p b
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ min (Int.int_val p (a.b1 * b.b1 + -(a.b2 * b.b2))) (Int.int_val p (a.b2 * b.b1 + a.b1 * b.b2)) =
    min (Int.int_val p a.b1) (Int.int_val p a.b2) + min (Int.int_val p b.b1) (Int.int_val p b.b2)