rw [rt7_sq]
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * rt7 ^ 2 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * 7 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2