big_int_ring_example
⊢ (p1 * p1 + q1 * q1 + r1 * r1 + s1 * s1 + t1 * t1 + u1 * u1 + v1 * v1 +
w1 * w1) *
(p2 * p2 + q2 * q2 + r2 * r2 + s2 * s2 + t2 * t2 + u2 * u2 + v2 * v2 +
w2 * w2) =
(p1 * p2 − q1 * q2 − r1 * r2 − s1 * s2 − t1 * t2 − u1 * u2 − v1 * v2 −
w1 * w2) *
(p1 * p2 − q1 * q2 − r1 * r2 − s1 * s2 − t1 * t2 − u1 * u2 − v1 * v2 −
w1 * w2) +
(p1 * q2 + q1 * p2 + r1 * s2 − s1 * r2 + t1 * u2 − u1 * t2 − v1 * w2 +
w1 * v2) *
(p1 * q2 + q1 * p2 + r1 * s2 − s1 * r2 + t1 * u2 − u1 * t2 − v1 * w2 +
w1 * v2) +
(p1 * r2 − q1 * s2 + r1 * p2 + s1 * q2 + t1 * v2 + u1 * w2 − v1 * t2 −
w1 * u2) *
(p1 * r2 − q1 * s2 + r1 * p2 + s1 * q2 + t1 * v2 + u1 * w2 − v1 * t2 −
w1 * u2) +
(p1 * s2 + q1 * r2 − r1 * q2 + s1 * p2 + t1 * w2 − u1 * v2 + v1 * u2 −
w1 * t2) *
(p1 * s2 + q1 * r2 − r1 * q2 + s1 * p2 + t1 * w2 − u1 * v2 + v1 * u2 −
w1 * t2) +
(p1 * t2 − q1 * u2 − r1 * v2 − s1 * w2 + t1 * p2 + u1 * q2 + v1 * r2 +
w1 * s2) *
(p1 * t2 − q1 * u2 − r1 * v2 − s1 * w2 + t1 * p2 + u1 * q2 + v1 * r2 +
w1 * s2) +
(p1 * u2 + q1 * t2 − r1 * w2 + s1 * v2 − t1 * q2 + u1 * p2 − v1 * s2 +
w1 * r2) *
(p1 * u2 + q1 * t2 − r1 * w2 + s1 * v2 − t1 * q2 + u1 * p2 − v1 * s2 +
w1 * r2) +
(p1 * v2 + q1 * w2 + r1 * t2 − s1 * u2 − t1 * r2 + u1 * s2 + v1 * p2 −
w1 * q2) *
(p1 * v2 + q1 * w2 + r1 * t2 − s1 * u2 − t1 * r2 + u1 * s2 + v1 * p2 −
w1 * q2) +
(p1 * w2 − q1 * v2 + r1 * u2 + s1 * t2 − t1 * s2 − u1 * r2 + v1 * q2 +
w1 * p2) *
(p1 * w2 − q1 * v2 + r1 * u2 + s1 * t2 − t1 * s2 − u1 * r2 + v1 * q2 +
w1 * p2)