Euler circle

Geogebra sheet

Coq statement

Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point,
  middle A B C1 -> middle B C A1 -> middle C A B1 ->
  orthogonal A B C C2 -> collinear A B C2 ->
  orthogonal B C A A2 -> collinear B C A2 ->
  orthogonal A C B B2 -> collinear A C B2 ->
  distance2 O A1 = distance2 O B1 ->
  distance2 O A1 = distance2 O C1 ->
  (distance2 O A2 = distance2 O A1
   /\distance2 O B2 = distance2 O A1
   /\distance2 O C2 = distance2 O A1)
  \/ collinear A B C.
Proof. geo_begin. tzR. tzR. tzR. Qed. 

Algebraic version

First goal
p:=  (1) *c^2*h*i +  (1) *d^2*h*i +  ((-1)) *c^2*h*j +  ((-1)) *d^2*h*j +  ((-1)) *c^2*g*k +  ((-1)) *d^2*g*k +  (1) *c^2*j*k +  (1) *d^2*j*k +  (1) *c^2*g*l +  (1) *d^2*g*l +  ((-1)) *c^2*i*l +  ((-1)) *d^2*i*l +  ((-2)) *c*h*i*q +  (2) *c*h*j*q +  (2) *c*g*k*q +  ((-2)) *c*j*k*q +  ((-2)) *c*g*l*q +  (2) *c*i*l*q +  (2) *h*i*q*r +  ((-2)) *h*j*q*r +  ((-2)) *g*k*q*r +  (2) *j*k*q*r +  (2) *g*l*q*r +  ((-2)) *i*l*q*r +  ((-1)) *h*i*r^2 +  (1) *h*j*r^2 +  (1) *g*k*r^2 +  ((-1)) *j*k*r^2 +  ((-1)) *g*l*r^2 +  (1) *i*l*r^2 +  ((-2)) *d*h*i*s +  (2) *d*h*j*s +  (2) *d*g*k*s +  ((-2)) *d*j*k*s +  ((-2)) *d*g*l*s +  (2) *d*i*l*s +  (2) *h*i*s*t +  ((-2)) *h*j*s*t +  ((-2)) *g*k*s*t +  (2) *j*k*s*t +  (2) *g*l*s*t +  ((-2)) *i*l*s*t +  ((-1)) *h*i*t^2 +  (1) *h*j*t^2 +  (1) *g*k*t^2 +  ((-1)) *j*k*t^2 +  ((-1)) *g*l*t^2 +  (1) *i*l*t^2 
F:= [
 ((-1)) *o^2 +  ((-1)) *p^2 +  (2) *o*q +  ((-2)) *q*r +  (1) *r^2 +  (2) *p*s +  ((-2)) *s*t +  (1) *t^2 ;
 ((-1)) *m^2 +  ((-1)) *n^2 +  (2) *m*q +  ((-2)) *q*r +  (1) *r^2 +  (2) *n*s +  ((-2)) *s*t +  (1) *t^2 ;
 ((-1)) *k +  ((-1)) *l +  (2) *p ;
 ((-1)) *i +  ((-1)) *j +  (2) *o ;
 ((-1)) *h +  ((-1)) *l +  (2) *t ;
 ((-1)) *g +  ((-1)) *j +  (2) *r ;
 ((-1)) *h +  ((-1)) *k +  (2) *n ;
 ((-1)) *g +  ((-1)) *i +  (2) *m ;
 (1) *e*g +  (1) *f*h +  ((-1)) *e*i +  ((-1)) *g*j +  (1) *i*j +  ((-1)) *f*k +  ((-1)) *h*l +  (1) *k*l ;
 (1) *f*g +  ((-1)) *e*h +  ((-1)) *f*i +  (1) *h*i +  (1) *e*k +  ((-1)) *g*k ;
 ((-1)) *c*g +  ((-1)) *d*h +  (1) *g*i +  (1) *c*j +  ((-1)) *i*j +  (1) *h*k +  (1) *d*l +  ((-1)) *k*l ;
 ((-1)) *d*g +  (1) *c*h +  (1) *d*j +  ((-1)) *h*j +  ((-1)) *c*l +  (1) *g*l ;
 ((-1)) *a*i +  (1) *g*i +  (1) *a*j +  ((-1)) *g*j +  ((-1)) *b*k +  (1) *h*k +  (1) *b*l +  ((-1)) *h*l ;
 ((-1)) *b*i +  (1) *b*j +  (1) *a*k +  ((-1)) *j*k +  ((-1)) *a*l +  (1) *i*l ;
];
Second goal
p:=  (1) *a^2*h*i +  (1) *b^2*h*i +  ((-1)) *a^2*h*j +  ((-1)) *b^2*h*j +  ((-1)) *a^2*g*k +  ((-1)) *b^2*g*k +  (1) *a^2*j*k +  (1) *b^2*j*k +  (1) *a^2*g*l +  (1) *b^2*g*l +  ((-1)) *a^2*i*l +  ((-1)) *b^2*i*l +  ((-2)) *a*h*i*q +  (2) *a*h*j*q +  (2) *a*g*k*q +  ((-2)) *a*j*k*q +  ((-2)) *a*g*l*q +  (2) *a*i*l*q +  (2) *h*i*q*r +  ((-2)) *h*j*q*r +  ((-2)) *g*k*q*r +  (2) *j*k*q*r +  (2) *g*l*q*r +  ((-2)) *i*l*q*r +  ((-1)) *h*i*r^2 +  (1) *h*j*r^2 +  (1) *g*k*r^2 +  ((-1)) *j*k*r^2 +  ((-1)) *g*l*r^2 +  (1) *i*l*r^2 +  ((-2)) *b*h*i*s +  (2) *b*h*j*s +  (2) *b*g*k*s +  ((-2)) *b*j*k*s +  ((-2)) *b*g*l*s +  (2) *b*i*l*s +  (2) *h*i*s*t +  ((-2)) *h*j*s*t +  ((-2)) *g*k*s*t +  (2) *j*k*s*t +  (2) *g*l*s*t +  ((-2)) *i*l*s*t +  ((-1)) *h*i*t^2 +  (1) *h*j*t^2 +  (1) *g*k*t^2 +  ((-1)) *j*k*t^2 +  ((-1)) *g*l*t^2 +  (1) *i*l*t^2 
F:= [
 ((-1)) *o^2 +  ((-1)) *p^2 +  (2) *o*q +  ((-2)) *q*r +  (1) *r^2 +  (2) *p*s +  ((-2)) *s*t +  (1) *t^2 ;
 ((-1)) *m^2 +  ((-1)) *n^2 +  (2) *m*q +  ((-2)) *q*r +  (1) *r^2 +  (2) *n*s +  ((-2)) *s*t +  (1) *t^2 ;
 ((-1)) *k +  ((-1)) *l +  (2) *p ;
 ((-1)) *i +  ((-1)) *j +  (2) *o ;
 ((-1)) *h +  ((-1)) *l +  (2) *t ;
 ((-1)) *g +  ((-1)) *j +  (2) *r ;
 ((-1)) *h +  ((-1)) *k +  (2) *n ;
 ((-1)) *g +  ((-1)) *i +  (2) *m ;
 (1) *e*g +  (1) *f*h +  ((-1)) *e*i +  ((-1)) *g*j +  (1) *i*j +  ((-1)) *f*k +  ((-1)) *h*l +  (1) *k*l ;
 (1) *f*g +  ((-1)) *e*h +  ((-1)) *f*i +  (1) *h*i +  (1) *e*k +  ((-1)) *g*k ;
 ((-1)) *c*g +  ((-1)) *d*h +  (1) *g*i +  (1) *c*j +  ((-1)) *i*j +  (1) *h*k +  (1) *d*l +  ((-1)) *k*l ;
 ((-1)) *d*g +  (1) *c*h +  (1) *d*j +  ((-1)) *h*j +  ((-1)) *c*l +  (1) *g*l ;
 ((-1)) *a*i +  (1) *g*i +  (1) *a*j +  ((-1)) *g*j +  ((-1)) *b*k +  (1) *h*k +  (1) *b*l +  ((-1)) *h*l ;
 ((-1)) *b*i +  (1) *b*j +  (1) *a*k +  ((-1)) *j*k +  ((-1)) *a*l +  (1) *i*l ;
];
Third goal
p:=  (1) *e^2*h*i +  (1) *f^2*h*i +  ((-1)) *e^2*h*j +  ((-1)) *f^2*h*j +  ((-1)) *e^2*g*k +  ((-1)) *f^2*g*k +  (1) *e^2*j*k +  (1) *f^2*j*k +  (1) *e^2*g*l +  (1) *f^2*g*l +  ((-1)) *e^2*i*l +  ((-1)) *f^2*i*l +  ((-2)) *e*h*i*q +  (2) *e*h*j*q +  (2) *e*g*k*q +  ((-2)) *e*j*k*q +  ((-2)) *e*g*l*q +  (2) *e*i*l*q +  (2) *h*i*q*r +  ((-2)) *h*j*q*r +  ((-2)) *g*k*q*r +  (2) *j*k*q*r +  (2) *g*l*q*r +  ((-2)) *i*l*q*r +  ((-1)) *h*i*r^2 +  (1) *h*j*r^2 +  (1) *g*k*r^2 +  ((-1)) *j*k*r^2 +  ((-1)) *g*l*r^2 +  (1) *i*l*r^2 +  ((-2)) *f*h*i*s +  (2) *f*h*j*s +  (2) *f*g*k*s +  ((-2)) *f*j*k*s +  ((-2)) *f*g*l*s +  (2) *f*i*l*s +  (2) *h*i*s*t +  ((-2)) *h*j*s*t +  ((-2)) *g*k*s*t +  (2) *j*k*s*t +  (2) *g*l*s*t +  ((-2)) *i*l*s*t +  ((-1)) *h*i*t^2 +  (1) *h*j*t^2 +  (1) *g*k*t^2 +  ((-1)) *j*k*t^2 +  ((-1)) *g*l*t^2 +  (1) *i*l*t^2 
F:= [
 ((-1)) *o^2 +  ((-1)) *p^2 +  (2) *o*q +  ((-2)) *q*r +  (1) *r^2 +  (2) *p*s +  ((-2)) *s*t +  (1) *t^2 ;
 ((-1)) *m^2 +  ((-1)) *n^2 +  (2) *m*q +  ((-2)) *q*r +  (1) *r^2 +  (2) *n*s +  ((-2)) *s*t +  (1) *t^2 ;
 ((-1)) *k +  ((-1)) *l +  (2) *p ;
 ((-1)) *i +  ((-1)) *j +  (2) *o ;
 ((-1)) *h +  ((-1)) *l +  (2) *t ;
 ((-1)) *g +  ((-1)) *j +  (2) *r ;
 ((-1)) *h +  ((-1)) *k +  (2) *n ;
 ((-1)) *g +  ((-1)) *i +  (2) *m ;
 (1) *e*g +  (1) *f*h +  ((-1)) *e*i +  ((-1)) *g*j +  (1) *i*j +  ((-1)) *f*k +  ((-1)) *h*l +  (1) *k*l ;
 (1) *f*g +  ((-1)) *e*h +  ((-1)) *f*i +  (1) *h*i +  (1) *e*k +  ((-1)) *g*k ;
 ((-1)) *c*g +  ((-1)) *d*h +  (1) *g*i +  (1) *c*j +  ((-1)) *i*j +  (1) *h*k +  (1) *d*l +  ((-1)) *k*l ;
 ((-1)) *d*g +  (1) *c*h +  (1) *d*j +  ((-1)) *h*j +  ((-1)) *c*l +  (1) *g*l ;
 ((-1)) *a*i +  (1) *g*i +  (1) *a*j +  ((-1)) *g*j +  ((-1)) *b*k +  (1) *h*k +  (1) *b*l +  ((-1)) *h*l ;
 ((-1)) *b*i +  (1) *b*j +  (1) *a*k +  ((-1)) *j*k +  ((-1)) *a*l +  (1) *i*l ;
];

Certificates

First certificate
CR:=[
 (1) *d +  ((-1)) *t ;  ((-2)) *r ;  (1) *c +  ((-2)) *q +  (1) *r ;  (1) *d*p +  (4) *q*r +  ((-2)) *r^2 +  ((-2)) *n*s +  ((-2)) *p*s +  ((-2)) *d*t +  (2) *n*t +  (1) *p*t +  (4) *s*t +  ((-2)) *t^2 ;  (1) *c*p +  (2) *n*q +  ((-2)) *n*r +  ((-1)) *p*r +  ((-2)) *c*t ;  (1) *c*n*o +  (2) *c^2*p +  (2) *d^2*p +  (1) *c*m*p +  (1) *c*o*p +  (1) *d*p^2 +  ((-2)) *d*m*q +  (2) *m*n*q +  ((-2)) *d*o*q +  ((-4)) *c*p*q +  ((-2)) *m*n*r +  (2) *d*o*r +  ((-1)) *n*o*r +  ((-1)) *m*p*r +  ((-1)) *o*p*r +  (4) *d*q*r +  (4) *p*q*r +  ((-2)) *d*r^2 +  ((-2)) *p*r^2 +  ((-2)) *d*n*s +  ((-6)) *d*p*s +  ((-2)) *c^2*t +  ((-2)) *d^2*t +  ((-1)) *c*m*t +  (1) *d*n*t +  ((-1)) *c*o*t +  (1) *d*p*t +  ((-1)) *p^2*t +  (4) *c*q*t +  ((-2)) *c*r*t +  (1) *m*r*t +  (1) *o*r*t +  ((-4)) *q*r*t +  (2) *r^2*t +  (8) *d*s*t +  (4) *p*s*t +  ((-4)) *d*t^2 +  (1) *n*t^2 +  ((-1)) *p*t^2 +  ((-4)) *s*t^2 +  (2) *t^3 ;  ((-2)) *c^2*o +  ((-2)) *d^2*o +  ((-1)) *d*n*o +  ((-1)) *d*m*p +  (2) *c*n*p +  ((-1)) *d*o*p +  (1) *c*p^2 +  (2) *n^2*q +  (4) *c*o*q +  (2) *c^2*r +  (2) *d^2*r +  ((-1)) *c*m*r +  (1) *d*n*r +  ((-2)) *n^2*r +  ((-1)) *c*o*r +  (1) *d*p*r +  ((-2)) *n*p*r +  ((-1)) *p^2*r +  ((-4)) *c*q*r +  (2) *m*q*r +  ((-2)) *o*q*r +  (2) *c*r^2 +  ((-1)) *m*r^2 +  (1) *o*r^2 +  (4) *d*o*s +  ((-4)) *d*r*s +  (2) *n*r*s +  (2) *p*r*s +  ((-2)) *c*n*t +  (1) *n*o*t +  ((-2)) *c*p*t +  (1) *m*p*t +  (1) *o*p*t +  (2) *d*r*t +  ((-1)) *n*r*t +  ((-1)) *p*r*t +  ((-4)) *o*s*t +  (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *c^2*l +  (2) *d^2*l +  ((-2)) *c*n*o +  ((-2)) *c^2*p +  ((-2)) *d^2*p +  ((-2)) *c*o*p +  ((-2)) *d*p^2 +  ((-4)) *c*l*q +  (4) *d*o*q +  (4) *c*p*q +  ((-4)) *d*o*r +  (2) *n*o*r +  (2) *o*p*r +  ((-4)) *d*q*r +  (4) *l*q*r +  ((-4)) *p*q*r +  (2) *d*r^2 +  ((-2)) *l*r^2 +  (2) *p*r^2 +  ((-4)) *d*l*s +  (8) *d*p*s +  (4) *c*o*t +  (2) *p^2*t +  ((-4)) *o*q*t +  (4) *q*r*t +  ((-2)) *r^2*t +  ((-4)) *d*s*t +  (4) *l*s*t +  ((-8)) *p*s*t +  (2) *d*t^2 +  ((-2)) *l*t^2 +  (2) *p*t^2 +  (4) *s*t^2 +  ((-2)) *t^3 ;  ((-2)) *c^2*j +  ((-2)) *d^2*j +  (2) *c^2*o +  (2) *d^2*o +  (2) *d*m*p +  ((-2)) *c*n*p +  (2) *d*o*p +  ((-2)) *c*p^2 +  (4) *c*j*q +  ((-4)) *c*o*q +  ((-4)) *d*p*r +  (2) *n*p*r +  (2) *p^2*r +  ((-4)) *j*q*r +  (4) *o*q*r +  (2) *j*r^2 +  ((-2)) *o*r^2 +  (4) *d*j*s +  ((-4)) *d*o*s +  (4) *c*p*t +  ((-2)) *m*p*t +  ((-2)) *o*p*t +  ((-4)) *j*s*t +  (4) *o*s*t +  (2) *j*t^2 +  ((-2)) *o*t^2 ;  (1) *c^2*h +  (1) *d^2*h +  ((-1)) *c^2*l +  ((-1)) *d^2*l +  ((-2)) *c*h*q +  (2) *c*l*q +  (2) *h*q*r +  ((-2)) *l*q*r +  ((-1)) *h*r^2 +  (1) *l*r^2 +  ((-2)) *d*h*s +  (2) *d*l*s +  (2) *h*s*t +  ((-2)) *l*s*t +  ((-1)) *h*t^2 +  (1) *l*t^2 ;  ((-1)) *c^2*g +  ((-1)) *d^2*g +  (1) *c^2*j +  (1) *d^2*j +  (2) *c*g*q +  ((-2)) *c*j*q +  ((-2)) *g*q*r +  (2) *j*q*r +  (1) *g*r^2 +  ((-1)) *j*r^2 +  (2) *d*g*s +  ((-2)) *d*j*s +  ((-2)) *g*s*t +  (2) *j*s*t +  (1) *g*t^2 +  ((-1)) *j*t^2 ;  ((-2)) *c*p +  (4) *d*q +  ((-4)) *n*q +  (4) *n*r +  (2) *p*r +  (2) *c*t +  ((-2)) *r*t ;  (2) *d*g +  ((-4)) *d*m +  (2) *c*n +  (2) *c*p +  (2) *d*r +  ((-2)) *n*r +  ((-2)) *p*r +  ((-4)) *c*t +  ((-2)) *g*t +  (4) *m*t +  (2) *r*t ; ];

C:=[
[
 (1) *d +  ((-1)) *t ;  ((-2)) *r ;  (1) *c +  ((-2)) *q +  (1) *r ;  (1) *d*p +  (4) *q*r +  ((-2)) *r^2 +  ((-2)) *n*s +  ((-2)) *p*s +  ((-2)) *d*t +  (2) *n*t +  (1) *p*t +  (4) *s*t +  ((-2)) *t^2 ;  (1) *c*p +  (2) *n*q +  ((-2)) *n*r +  ((-1)) *p*r +  ((-2)) *c*t ;  (1) *c*n*o +  (2) *c^2*p +  (2) *d^2*p +  (1) *c*m*p +  (1) *c*o*p +  (1) *d*p^2 +  ((-2)) *d*m*q +  (2) *m*n*q +  ((-2)) *d*o*q +  ((-4)) *c*p*q +  ((-2)) *m*n*r +  (2) *d*o*r +  ((-1)) *n*o*r +  ((-1)) *m*p*r +  ((-1)) *o*p*r +  (4) *d*q*r +  (4) *p*q*r +  ((-2)) *d*r^2 +  ((-2)) *p*r^2 +  ((-2)) *d*n*s +  ((-6)) *d*p*s +  ((-2)) *c^2*t +  ((-2)) *d^2*t +  ((-1)) *c*m*t +  (1) *d*n*t +  ((-1)) *c*o*t +  (1) *d*p*t +  ((-1)) *p^2*t +  (4) *c*q*t +  ((-2)) *c*r*t +  (1) *m*r*t +  (1) *o*r*t +  ((-4)) *q*r*t +  (2) *r^2*t +  (8) *d*s*t +  (4) *p*s*t +  ((-4)) *d*t^2 +  (1) *n*t^2 +  ((-1)) *p*t^2 +  ((-4)) *s*t^2 +  (2) *t^3 ;  ((-2)) *c^2*o +  ((-2)) *d^2*o +  ((-1)) *d*n*o +  ((-1)) *d*m*p +  (2) *c*n*p +  ((-1)) *d*o*p +  (1) *c*p^2 +  (2) *n^2*q +  (4) *c*o*q +  (2) *c^2*r +  (2) *d^2*r +  ((-1)) *c*m*r +  (1) *d*n*r +  ((-2)) *n^2*r +  ((-1)) *c*o*r +  (1) *d*p*r +  ((-2)) *n*p*r +  ((-1)) *p^2*r +  ((-4)) *c*q*r +  (2) *m*q*r +  ((-2)) *o*q*r +  (2) *c*r^2 +  ((-1)) *m*r^2 +  (1) *o*r^2 +  (4) *d*o*s +  ((-4)) *d*r*s +  (2) *n*r*s +  (2) *p*r*s +  ((-2)) *c*n*t +  (1) *n*o*t +  ((-2)) *c*p*t +  (1) *m*p*t +  (1) *o*p*t +  (2) *d*r*t +  ((-1)) *n*r*t +  ((-1)) *p*r*t +  ((-4)) *o*s*t +  (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *c^2*l +  (2) *d^2*l +  ((-2)) *c*n*o +  ((-2)) *c^2*p +  ((-2)) *d^2*p +  ((-2)) *c*o*p +  ((-2)) *d*p^2 +  ((-4)) *c*l*q +  (4) *d*o*q +  (4) *c*p*q +  ((-4)) *d*o*r +  (2) *n*o*r +  (2) *o*p*r +  ((-4)) *d*q*r +  (4) *l*q*r +  ((-4)) *p*q*r +  (2) *d*r^2 +  ((-2)) *l*r^2 +  (2) *p*r^2 +  ((-4)) *d*l*s +  (8) *d*p*s +  (4) *c*o*t +  (2) *p^2*t +  ((-4)) *o*q*t +  (4) *q*r*t +  ((-2)) *r^2*t +  ((-4)) *d*s*t +  (4) *l*s*t +  ((-8)) *p*s*t +  (2) *d*t^2 +  ((-2)) *l*t^2 +  (2) *p*t^2 +  (4) *s*t^2 +  ((-2)) *t^3 ;  ((-2)) *c^2*j +  ((-2)) *d^2*j +  (2) *c^2*o +  (2) *d^2*o +  (2) *d*m*p +  ((-2)) *c*n*p +  (2) *d*o*p +  ((-2)) *c*p^2 +  (4) *c*j*q +  ((-4)) *c*o*q +  ((-4)) *d*p*r +  (2) *n*p*r +  (2) *p^2*r +  ((-4)) *j*q*r +  (4) *o*q*r +  (2) *j*r^2 +  ((-2)) *o*r^2 +  (4) *d*j*s +  ((-4)) *d*o*s +  (4) *c*p*t +  ((-2)) *m*p*t +  ((-2)) *o*p*t +  ((-4)) *j*s*t +  (4) *o*s*t +  (2) *j*t^2 +  ((-2)) *o*t^2 ;  (1) *c^2*h +  (1) *d^2*h +  ((-1)) *c^2*l +  ((-1)) *d^2*l +  ((-2)) *c*h*q +  (2) *c*l*q +  (2) *h*q*r +  ((-2)) *l*q*r +  ((-1)) *h*r^2 +  (1) *l*r^2 +  ((-2)) *d*h*s +  (2) *d*l*s +  (2) *h*s*t +  ((-2)) *l*s*t +  ((-1)) *h*t^2 +  (1) *l*t^2 ;  ((-1)) *c^2*g +  ((-1)) *d^2*g +  (1) *c^2*j +  (1) *d^2*j +  (2) *c*g*q +  ((-2)) *c*j*q +  ((-2)) *g*q*r +  (2) *j*q*r +  (1) *g*r^2 +  ((-1)) *j*r^2 +  (2) *d*g*s +  ((-2)) *d*j*s +  ((-2)) *g*s*t +  (2) *j*s*t +  (1) *g*t^2 +  ((-1)) *j*t^2 ;  ((-2)) *c*p +  (4) *d*q +  ((-4)) *n*q +  (4) *n*r +  (2) *p*r +  (2) *c*t +  ((-2)) *r*t ;  (2) *d*g +  ((-4)) *d*m +  (2) *c*n +  (2) *c*p +  (2) *d*r +  ((-2)) *n*r +  ((-2)) *p*r +  ((-4)) *c*t +  ((-2)) *g*t +  (4) *m*t +  (2) *r*t ; ];

[
0; 0;  (1) *n ;  ((-1)) *m +  ((-1)) *o ;  (1) *n^2 +  ((-2)) *m*o ;  ((-1)) *m*n ; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *m*o ; 0; 0; 0;  ((-2)) *c +  ((-2)) *j +  (4) *o ; 0; ];

[
0;  (1) *c ;  ((-1)) *d ;  ((-1)) *d*m ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *d ; 0; ];

[
 (1) *m +  (1) *o ;  (1) *n ;  (1) *m*n ;  (1) *n^2 ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *d +  ((-2)) *n ; 0; ];

[
0; 0;  (1) *c ; 0; 0;  ((-1))  ; 0; 0; 0;  (1) *d ; 0;  ((-1)) *l ;  ((-1)) *c +  (1) *j ;  ((-1)) *d ; 0; 0; 0; ];

[
 ((-1)) *j ;  ((-1)) *d +  ((-1)) *l ; 0; 0; 0;  ((-1))  ; 0; 0;  (1) *c ; 0;  (1) *j ;  (1) *d +  (1) *l ;  ((-1)) *c +  ((-1)) *g +  (1) *j ;  ((-1)) *h +  (1) *l ; 0; 0; ];

[
0; 0; 0; 0; 0; 0; 0;  ((-1))  ; 0;  (1)  ; 0;  (1)  ; 0; 0; 0; ];

[
0; 0; 0; 0; 0; 0; 0;  ((-1))  ; 0;  (1)  ; 0;  (1)  ; 0; 0; ];

];

c:=
(-1);
Second certificate
CR:=[
 (2) *o +  ((-2)) *r ;  (2) *b*p +  ((-2)) *o*r +  (2) *r^2 +  ((-2)) *b*t +  ((-2)) *p*t +  (2) *t^2 ;  (2) *a*p +  ((-2)) *p*r +  ((-2)) *a*t +  (2) *o*t ;  (2) *a^2*p +  (2) *b^2*p +  (2) *a*m*p +  (2) *a*o*p +  (2) *b*p^2 +  ((-4)) *a*p*q +  ((-2)) *b*o*r +  ((-2)) *m*p*r +  ((-2)) *o*p*r +  (4) *p*q*r +  (2) *b*r^2 +  ((-2)) *p*r^2 +  ((-4)) *b*p*s +  ((-2)) *a^2*t +  ((-2)) *b^2*t +  ((-2)) *a*m*t +  (2) *m*o*t +  ((-2)) *b*p*t +  ((-2)) *p^2*t +  (4) *a*q*t +  ((-2)) *a*r*t +  (2) *o*r*t +  ((-4)) *q*r*t +  (2) *r^2*t +  (4) *b*s*t +  (4) *p*s*t +  ((-4)) *s*t^2 +  (2) *t^3 ;  ((-2)) *a^2*o +  ((-2)) *b^2*o +  ((-2)) *b*n*o +  (2) *a*n*p +  ((-2)) *b*o*p +  (2) *a*p^2 +  (2) *a^2*r +  (2) *b^2*r +  (2) *b*n*r +  (2) *a*o*r +  ((-2)) *n*p*r +  ((-2)) *p^2*r +  ((-2)) *a*r^2 +  (4) *b*o*s +  ((-4)) *a*p*s +  ((-4)) *b*r*s +  (4) *p*r*s +  ((-2)) *a*n*t +  (2) *n*o*t +  (2) *a*p*t +  (2) *o*p*t +  (2) *b*r*t +  ((-2)) *p*r*t +  (4) *a*s*t +  ((-4)) *o*s*t +  ((-4)) *a*t^2 +  (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *a^2*l +  (2) *b^2*l +  ((-2)) *a^2*p +  ((-2)) *b^2*p +  ((-4)) *a*o*p +  ((-4)) *b*p^2 +  ((-4)) *a*l*q +  (8) *b*o*q +  (4) *a*p*q +  ((-4)) *b*o*r +  (4) *o*p*r +  ((-8)) *b*q*r +  (4) *l*q*r +  ((-4)) *p*q*r +  (4) *b*r^2 +  ((-2)) *l*r^2 +  (2) *p*r^2 +  ((-4)) *b*l*s +  (12) *b*p*s +  (4) *a*o*t +  (4) *p^2*t +  ((-8)) *o*q*t +  (8) *q*r*t +  ((-4)) *r^2*t +  ((-8)) *b*s*t +  (4) *l*s*t +  ((-12)) *p*s*t +  (4) *b*t^2 +  ((-2)) *l*t^2 +  (2) *p*t^2 +  (8) *s*t^2 +  ((-4)) *t^3 ;  ((-2)) *a^2*j +  ((-2)) *b^2*j +  (2) *a^2*o +  (2) *b^2*o +  (4) *b*o*p +  ((-4)) *a*p^2 +  (4) *a*j*q +  ((-4)) *a*o*q +  ((-4)) *b*p*r +  (4) *p^2*r +  ((-4)) *j*q*r +  (4) *o*q*r +  (2) *j*r^2 +  ((-2)) *o*r^2 +  (4) *b*j*s +  ((-4)) *b*o*s +  (4) *a*p*t +  ((-4)) *o*p*t +  ((-4)) *j*s*t +  (4) *o*s*t +  (2) *j*t^2 +  ((-2)) *o*t^2 ;  (1) *a^2*h +  (1) *b^2*h +  ((-1)) *a^2*l +  ((-1)) *b^2*l +  ((-2)) *a*h*q +  (2) *a*l*q +  (2) *h*q*r +  ((-2)) *l*q*r +  ((-1)) *h*r^2 +  (1) *l*r^2 +  ((-2)) *b*h*s +  (2) *b*l*s +  (2) *h*s*t +  ((-2)) *l*s*t +  ((-1)) *h*t^2 +  (1) *l*t^2 ;  ((-1)) *a^2*g +  ((-1)) *b^2*g +  (1) *a^2*j +  (1) *b^2*j +  (2) *a*g*q +  ((-2)) *a*j*q +  ((-2)) *g*q*r +  (2) *j*q*r +  (1) *g*r^2 +  ((-1)) *j*r^2 +  (2) *b*g*s +  ((-2)) *b*j*s +  ((-2)) *g*s*t +  (2) *j*s*t +  (1) *g*t^2 +  ((-1)) *j*t^2 ;  ((-4)) *a*p +  (4) *p*r +  (4) *a*t +  ((-4)) *o*t ;  (4) *b*g +  (4) *b*j +  ((-4)) *a*l +  ((-4)) *b*m +  (4) *a*p +  ((-4)) *b*r +  (4) *l*r +  ((-4)) *p*r +  ((-4)) *g*t +  ((-4)) *j*t +  (4) *m*t +  (4) *r*t ; ];

C:=[
[
 (2) *o +  ((-2)) *r ;  (2) *b*p +  ((-2)) *o*r +  (2) *r^2 +  ((-2)) *b*t +  ((-2)) *p*t +  (2) *t^2 ;  (2) *a*p +  ((-2)) *p*r +  ((-2)) *a*t +  (2) *o*t ;  (2) *a^2*p +  (2) *b^2*p +  (2) *a*m*p +  (2) *a*o*p +  (2) *b*p^2 +  ((-4)) *a*p*q +  ((-2)) *b*o*r +  ((-2)) *m*p*r +  ((-2)) *o*p*r +  (4) *p*q*r +  (2) *b*r^2 +  ((-2)) *p*r^2 +  ((-4)) *b*p*s +  ((-2)) *a^2*t +  ((-2)) *b^2*t +  ((-2)) *a*m*t +  (2) *m*o*t +  ((-2)) *b*p*t +  ((-2)) *p^2*t +  (4) *a*q*t +  ((-2)) *a*r*t +  (2) *o*r*t +  ((-4)) *q*r*t +  (2) *r^2*t +  (4) *b*s*t +  (4) *p*s*t +  ((-4)) *s*t^2 +  (2) *t^3 ;  ((-2)) *a^2*o +  ((-2)) *b^2*o +  ((-2)) *b*n*o +  (2) *a*n*p +  ((-2)) *b*o*p +  (2) *a*p^2 +  (2) *a^2*r +  (2) *b^2*r +  (2) *b*n*r +  (2) *a*o*r +  ((-2)) *n*p*r +  ((-2)) *p^2*r +  ((-2)) *a*r^2 +  (4) *b*o*s +  ((-4)) *a*p*s +  ((-4)) *b*r*s +  (4) *p*r*s +  ((-2)) *a*n*t +  (2) *n*o*t +  (2) *a*p*t +  (2) *o*p*t +  (2) *b*r*t +  ((-2)) *p*r*t +  (4) *a*s*t +  ((-4)) *o*s*t +  ((-4)) *a*t^2 +  (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *a^2*l +  (2) *b^2*l +  ((-2)) *a^2*p +  ((-2)) *b^2*p +  ((-4)) *a*o*p +  ((-4)) *b*p^2 +  ((-4)) *a*l*q +  (8) *b*o*q +  (4) *a*p*q +  ((-4)) *b*o*r +  (4) *o*p*r +  ((-8)) *b*q*r +  (4) *l*q*r +  ((-4)) *p*q*r +  (4) *b*r^2 +  ((-2)) *l*r^2 +  (2) *p*r^2 +  ((-4)) *b*l*s +  (12) *b*p*s +  (4) *a*o*t +  (4) *p^2*t +  ((-8)) *o*q*t +  (8) *q*r*t +  ((-4)) *r^2*t +  ((-8)) *b*s*t +  (4) *l*s*t +  ((-12)) *p*s*t +  (4) *b*t^2 +  ((-2)) *l*t^2 +  (2) *p*t^2 +  (8) *s*t^2 +  ((-4)) *t^3 ;  ((-2)) *a^2*j +  ((-2)) *b^2*j +  (2) *a^2*o +  (2) *b^2*o +  (4) *b*o*p +  ((-4)) *a*p^2 +  (4) *a*j*q +  ((-4)) *a*o*q +  ((-4)) *b*p*r +  (4) *p^2*r +  ((-4)) *j*q*r +  (4) *o*q*r +  (2) *j*r^2 +  ((-2)) *o*r^2 +  (4) *b*j*s +  ((-4)) *b*o*s +  (4) *a*p*t +  ((-4)) *o*p*t +  ((-4)) *j*s*t +  (4) *o*s*t +  (2) *j*t^2 +  ((-2)) *o*t^2 ;  (1) *a^2*h +  (1) *b^2*h +  ((-1)) *a^2*l +  ((-1)) *b^2*l +  ((-2)) *a*h*q +  (2) *a*l*q +  (2) *h*q*r +  ((-2)) *l*q*r +  ((-1)) *h*r^2 +  (1) *l*r^2 +  ((-2)) *b*h*s +  (2) *b*l*s +  (2) *h*s*t +  ((-2)) *l*s*t +  ((-1)) *h*t^2 +  (1) *l*t^2 ;  ((-1)) *a^2*g +  ((-1)) *b^2*g +  (1) *a^2*j +  (1) *b^2*j +  (2) *a*g*q +  ((-2)) *a*j*q +  ((-2)) *g*q*r +  (2) *j*q*r +  (1) *g*r^2 +  ((-1)) *j*r^2 +  (2) *b*g*s +  ((-2)) *b*j*s +  ((-2)) *g*s*t +  (2) *j*s*t +  (1) *g*t^2 +  ((-1)) *j*t^2 ;  ((-4)) *a*p +  (4) *p*r +  (4) *a*t +  ((-4)) *o*t ;  (4) *b*g +  (4) *b*j +  ((-4)) *a*l +  ((-4)) *b*m +  (4) *a*p +  ((-4)) *b*r +  (4) *l*r +  ((-4)) *p*r +  ((-4)) *g*t +  ((-4)) *j*t +  (4) *m*t +  (4) *r*t ; ];

[
 (1) *a ;  ((-1)) *b ;  ((-1)) *b*m ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0;  (2) *b ; 0; ];

[
0;  ((-1)) *b ;  (1) *a ;  ((-1))  ; 0; 0; 0; 0; 0; 0; 0; 0; 0;  (1) *b +  ((-1)) *l ;  ((-1)) *a +  (1) *j ; 0; 0; ];

[
 ((-1)) *a +  ((-1)) *j ;  ((-1)) *b +  ((-1)) *l ; 0;  ((-1))  ; 0; 0; 0; 0; 0; 0;  (2) *j ;  (2) *l ;  (1) *a +  ((-1)) *g ;  (1) *b +  ((-1)) *h ; 0; 0; ];

[
0; 0; 0; 0; 0; 0; 0;  ((-1))  ; 0;  (1)  ; 0;  (1)  ; 0; 0; 0; ];

[
0; 0; 0; 0; 0; 0; 0;  ((-1))  ; 0;  (1)  ; 0;  (1)  ; 0; 0; ];

];

c:=
(-1);
Third certificate
CR:=[
 (2) *m +  ((-2)) *r ;  ((-2)) *f*n +  ((-2)) *n^2 +  (4) *m*q +  ((-4)) *q*r +  (4) *n*s +  (2) *f*t +  (2) *n*t +  ((-4)) *s*t ;  ((-2)) *e*n +  (2) *m*n +  (2) *e*t +  ((-2)) *m*t ;  ((-2)) *e*n*o +  (2) *m*n*o +  ((-2)) *e^2*p +  ((-2)) *f^2*p +  ((-2)) *e*m*p +  ((-2)) *f*n*p +  (4) *e*p*q +  ((-2)) *f*m*r +  (2) *e*n*r +  (2) *e*p*r +  (2) *m*p*r +  ((-4)) *p*q*r +  (2) *f*r^2 +  ((-2)) *n*r^2 +  (4) *f*p*s +  (2) *e^2*t +  (2) *f^2*t +  (2) *e*m*t +  (2) *f*n*t +  (2) *e*o*t +  ((-2)) *m*o*t +  (2) *f*p*t +  (2) *n*p*t +  ((-4)) *e*q*t +  ((-4)) *e*r*t +  (4) *q*r*t +  ((-4)) *f*s*t +  ((-4)) *p*s*t +  ((-2)) *f*t^2 +  ((-2)) *n*t^2 +  (4) *s*t^2 ;  (2) *e^2*o +  (2) *f^2*o +  (2) *f*n*o +  (2) *n^2*o +  (2) *f*m*p +  ((-2)) *e*n*p +  ((-4)) *e*o*q +  ((-4)) *m*o*q +  ((-2)) *e^2*r +  ((-2)) *f^2*r +  ((-2)) *e*m*r +  ((-2)) *f*n*r +  ((-2)) *f*p*r +  (2) *n*p*r +  (4) *e*q*r +  (8) *o*q*r +  (2) *e*r^2 +  (2) *m*r^2 +  ((-2)) *o*r^2 +  ((-4)) *q*r^2 +  ((-4)) *f*o*s +  ((-4)) *n*o*s +  (4) *f*r*s +  ((-2)) *f*m*t +  (2) *e*n*t +  ((-2)) *f*o*t +  ((-2)) *n*o*t +  (2) *e*p*t +  ((-2)) *m*p*t +  (4) *f*r*t +  (8) *o*s*t +  ((-4)) *r*s*t +  ((-2)) *e*t^2 +  (2) *m*t^2 +  ((-2)) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0;  ((-2)) *e^2*l +  ((-2)) *f^2*l +  (2) *e^2*p +  (2) *f^2*p +  (4) *e*m*p +  (4) *f*n*p +  (4) *e*l*q +  ((-4)) *e*p*q +  ((-4)) *e*p*r +  ((-4)) *m*p*r +  ((-4)) *l*q*r +  (4) *p*q*r +  (2) *l*r^2 +  (2) *p*r^2 +  (4) *f*l*s +  ((-4)) *f*p*s +  ((-4)) *f*p*t +  ((-4)) *n*p*t +  ((-4)) *l*s*t +  (4) *p*s*t +  (2) *l*t^2 +  (2) *p*t^2 ;  (2) *e^2*j +  (2) *f^2*j +  ((-2)) *e^2*o +  ((-2)) *f^2*o +  ((-4)) *f*n*o +  ((-4)) *n^2*o +  ((-4)) *e*j*q +  (4) *e*o*q +  (8) *m*o*q +  (4) *j*q*r +  ((-12)) *o*q*r +  ((-2)) *j*r^2 +  (2) *o*r^2 +  ((-4)) *f*j*s +  (4) *f*o*s +  (8) *n*o*s +  (4) *f*o*t +  (4) *n*o*t +  (4) *j*s*t +  ((-12)) *o*s*t +  ((-2)) *j*t^2 +  (2) *o*t^2 ;  ((-1)) *e^2*h +  ((-1)) *f^2*h +  (1) *e^2*l +  (1) *f^2*l +  (2) *e*h*q +  ((-2)) *e*l*q +  ((-2)) *h*q*r +  (2) *l*q*r +  (1) *h*r^2 +  ((-1)) *l*r^2 +  (2) *f*h*s +  ((-2)) *f*l*s +  ((-2)) *h*s*t +  (2) *l*s*t +  (1) *h*t^2 +  ((-1)) *l*t^2 ;  (1) *e^2*g +  (1) *f^2*g +  ((-1)) *e^2*j +  ((-1)) *f^2*j +  ((-2)) *e*g*q +  (2) *e*j*q +  (2) *g*q*r +  ((-2)) *j*q*r +  ((-1)) *g*r^2 +  (1) *j*r^2 +  ((-2)) *f*g*s +  (2) *f*j*s +  (2) *g*s*t +  ((-2)) *j*s*t +  ((-1)) *g*t^2 +  (1) *j*t^2 ;  ((-4)) *n*o +  (4) *g*p +  (4) *o*p +  ((-4)) *l*r +  ((-4)) *p*r +  (4) *j*t ;  ((-4)) *e*n +  (4) *m*n +  (4) *e*t +  ((-4)) *m*t ; ];

C:=[
[
 (2) *m +  ((-2)) *r ;  ((-2)) *f*n +  ((-2)) *n^2 +  (4) *m*q +  ((-4)) *q*r +  (4) *n*s +  (2) *f*t +  (2) *n*t +  ((-4)) *s*t ;  ((-2)) *e*n +  (2) *m*n +  (2) *e*t +  ((-2)) *m*t ;  ((-2)) *e*n*o +  (2) *m*n*o +  ((-2)) *e^2*p +  ((-2)) *f^2*p +  ((-2)) *e*m*p +  ((-2)) *f*n*p +  (4) *e*p*q +  ((-2)) *f*m*r +  (2) *e*n*r +  (2) *e*p*r +  (2) *m*p*r +  ((-4)) *p*q*r +  (2) *f*r^2 +  ((-2)) *n*r^2 +  (4) *f*p*s +  (2) *e^2*t +  (2) *f^2*t +  (2) *e*m*t +  (2) *f*n*t +  (2) *e*o*t +  ((-2)) *m*o*t +  (2) *f*p*t +  (2) *n*p*t +  ((-4)) *e*q*t +  ((-4)) *e*r*t +  (4) *q*r*t +  ((-4)) *f*s*t +  ((-4)) *p*s*t +  ((-2)) *f*t^2 +  ((-2)) *n*t^2 +  (4) *s*t^2 ;  (2) *e^2*o +  (2) *f^2*o +  (2) *f*n*o +  (2) *n^2*o +  (2) *f*m*p +  ((-2)) *e*n*p +  ((-4)) *e*o*q +  ((-4)) *m*o*q +  ((-2)) *e^2*r +  ((-2)) *f^2*r +  ((-2)) *e*m*r +  ((-2)) *f*n*r +  ((-2)) *f*p*r +  (2) *n*p*r +  (4) *e*q*r +  (8) *o*q*r +  (2) *e*r^2 +  (2) *m*r^2 +  ((-2)) *o*r^2 +  ((-4)) *q*r^2 +  ((-4)) *f*o*s +  ((-4)) *n*o*s +  (4) *f*r*s +  ((-2)) *f*m*t +  (2) *e*n*t +  ((-2)) *f*o*t +  ((-2)) *n*o*t +  (2) *e*p*t +  ((-2)) *m*p*t +  (4) *f*r*t +  (8) *o*s*t +  ((-4)) *r*s*t +  ((-2)) *e*t^2 +  (2) *m*t^2 +  ((-2)) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0;  ((-2)) *e^2*l +  ((-2)) *f^2*l +  (2) *e^2*p +  (2) *f^2*p +  (4) *e*m*p +  (4) *f*n*p +  (4) *e*l*q +  ((-4)) *e*p*q +  ((-4)) *e*p*r +  ((-4)) *m*p*r +  ((-4)) *l*q*r +  (4) *p*q*r +  (2) *l*r^2 +  (2) *p*r^2 +  (4) *f*l*s +  ((-4)) *f*p*s +  ((-4)) *f*p*t +  ((-4)) *n*p*t +  ((-4)) *l*s*t +  (4) *p*s*t +  (2) *l*t^2 +  (2) *p*t^2 ;  (2) *e^2*j +  (2) *f^2*j +  ((-2)) *e^2*o +  ((-2)) *f^2*o +  ((-4)) *f*n*o +  ((-4)) *n^2*o +  ((-4)) *e*j*q +  (4) *e*o*q +  (8) *m*o*q +  (4) *j*q*r +  ((-12)) *o*q*r +  ((-2)) *j*r^2 +  (2) *o*r^2 +  ((-4)) *f*j*s +  (4) *f*o*s +  (8) *n*o*s +  (4) *f*o*t +  (4) *n*o*t +  (4) *j*s*t +  ((-12)) *o*s*t +  ((-2)) *j*t^2 +  (2) *o*t^2 ;  ((-1)) *e^2*h +  ((-1)) *f^2*h +  (1) *e^2*l +  (1) *f^2*l +  (2) *e*h*q +  ((-2)) *e*l*q +  ((-2)) *h*q*r +  (2) *l*q*r +  (1) *h*r^2 +  ((-1)) *l*r^2 +  (2) *f*h*s +  ((-2)) *f*l*s +  ((-2)) *h*s*t +  (2) *l*s*t +  (1) *h*t^2 +  ((-1)) *l*t^2 ;  (1) *e^2*g +  (1) *f^2*g +  ((-1)) *e^2*j +  ((-1)) *f^2*j +  ((-2)) *e*g*q +  (2) *e*j*q +  (2) *g*q*r +  ((-2)) *j*q*r +  ((-1)) *g*r^2 +  (1) *j*r^2 +  ((-2)) *f*g*s +  (2) *f*j*s +  (2) *g*s*t +  ((-2)) *j*s*t +  ((-1)) *g*t^2 +  (1) *j*t^2 ;  ((-4)) *n*o +  (4) *g*p +  (4) *o*p +  ((-4)) *l*r +  ((-4)) *p*r +  (4) *j*t ;  ((-4)) *e*n +  (4) *m*n +  (4) *e*t +  ((-4)) *m*t ; ];

[
 ((-1)) *e +  ((-1)) *m ;  (1) *f +  ((-1)) *n ;  (1) *f*o +  ((-1)) *n*o ;  (1) *e*o +  (1) *m*o ; 0; 0; 0; 0; 0; 0; 0; 0; 0;  ((-2)) *e*o +  ((-2)) *m*o ; 0; 0; 0;  (2) *f +  ((-2)) *n ; ];

[
0;  (1) *f ; 0; 0; 0; 0; 0;  (1)  ; 0;  (1) *f ; 0;  (1) *l ;  ((-1)) *e +  ((-1)) *j ;  ((-2)) *f +  (1) *h ;  (1) *e +  ((-1)) *g ; 0; 0; ];

[
 (1) *e ; 0; 0; 0; 0; 0; 0;  (1)  ;  (1) *e ; 0;  ((-1)) *j ;  (1) *f +  ((-1)) *l ;  ((-2)) *e +  (1) *j ;  ((-1)) *f +  (1) *l ; 0; 0; ];

[
0; 0; 0; 0; 0; 0; 0;  ((-1))  ; 0;  (1)  ; 0;  (1)  ; 0; 0; 0; ];

[
0; 0; 0; 0; 0; 0; 0;  ((-1))  ; 0;  (1)  ; 0;  (1)  ; 0; 0; ];

];

c:=
1;