# Feuerbach Theorem (Yang & Zhang, 1992)
FeuerbachA := Theorem(
   [-u1^3+4*u1^2*x1+4*u2^2*x1^2*u1-4*u2*x1^2*u1-4*u1*x1^2-8*u2^2*
    x1^3+8*u2*x1^3+4*x1^2*u1^3-8*x1^3*u1^2+4*u1*x1^4,
    -2*u2*x1-2*x1*x2+2*x1+2*u1*x2-u1, 4*u1*x3-u1^2-u2+u2^2, 4*x4-1-2*u2,
    u1^4-2*u1^2*u2+2*u1^2*u2^2+u2^2-2*u2^3+u2^4+u1^2-16*u1^2*x5],    
   ((x1-x3)^2+(x2-x4)^2)^2+x5^2+x1^4-2*((x1-x3)^2+(x2-x4)^2)*(x5+x1^2)
    -2*x5*x1^2,[x1,x2,x3,x4,x5]);
