Skip to content

Instantly share code, notes, and snippets.

@andres-erbsen

andres-erbsen/nsatz-weierstrass.v Secret

Created September 3, 2016 02:01
Show Gist options
  • Save andres-erbsen/bf8d8a98c490ff898aec23eb21ae75d8 to your computer and use it in GitHub Desktop.
Save andres-erbsen/bf8d8a98c490ff898aec23eb21ae75d8 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
nsatz-weierstrass.v
Require Import Coq.nsatz.Nsatz Coq.setoid_ring.Ring_tac Coq.QArith.QArith.
Local Open Scope Q_scope.
Local Notation "2" := (1+1).
Local Notation "3" := (1+1+1).
Goal forall
x1 y1 x2 y2 x3 y3 a b : Q,
y1^2-x1^3-a*x1-b == 0 ->
y2^2-x2^3-a*x2-b == 0 ->
y3^2-x3^3-a*x3-b == 0->
((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
(x3 - x2) * x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
(x3 - x2) * x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
(x3 - x2) * x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) *
(y2 - y1) +
((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
(x3 - x2) * x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
(x3 - x2) * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) *
(y2 - y1) +
((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
(x3 - x2) * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) *
(y2 - y1) +
((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * x2 *
x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * x3 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * x1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 *
x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
x3 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
x3 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
x3 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 *
x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (2 * (1 + 2 ^ 2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * (x2 - x1) * (x2 - x1) * (y2 - y1) *
(y2 - y1) * (y2 - y1) * (y2 - y1)
==
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x2 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x2 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x3 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x1 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x3 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x1 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 * x1 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 *
x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * y3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * ((2 * x1 + x2) * (y2 - y1)) *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 *
x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 *
x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * y3 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 *
((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 *
x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * y3 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 *
((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) -
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * y3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * ((2 * x1 + x2) * (y2 - y1)) *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * y3 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 *
((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * y3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * ((2 * x1 + x2) * (y2 - y1)) *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * y1 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * y1 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * y1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x2 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x2 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x3 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x1 * y3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 *
x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (2 * (1 + 2 ^ 2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * y3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x3 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * y3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 *
((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * y3 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) -
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 *
((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) +
2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * y1 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * y3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * (x2 - x1) * (x2 - x1) * (y2 - y1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * (x2 - x1) * (x2 - x1) *
(y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y3 * y3 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y3 *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
(x2 - x1) +
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y3 * (x2 - x1) * (x2 - x1) *
(x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
(x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * ((2 * x1 + x2) * (y2 - y1)) *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) *
((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
(y2 - y1).
Proof.
intros.
nsatz.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment