Chords

Coq statement

Lemma chords: forall O A B C D M:point,
  equaldistance O A O B ->
  equaldistance O A O C ->
  equaldistance O A O D ->
  collinear A B M -> collinear C D M ->
  scalarproduct A M B = scalarproduct C M D
  \/ parallel A B C D.
Proof. geo_begin. tzR. Qed.

Algebraic version

p:=  ((-1)) *b*c*d*g +  ((-1)) *a*d^2*g +  ((-1)) *b*d*e*g +  (1) *c*d*e*g +  (1) *b*c*f*g +  (1) *d^2*f*g +  (1) *b*e*f*g +  ((-1)) *c*e*f*g +  (1) *a*f^2*g +  ((-1)) *d*f^2*g +  (1) *b*d*g^2 +  ((-1)) *b*f*g^2 +  (1) *b*c^2*h +  (1) *a*c*d*h +  ((-1)) *c^2*e*h +  ((-1)) *a*d*e*h +  ((-1)) *b*e^2*h +  (1) *c*e^2*h +  (1) *a*c*f*h +  ((-1)) *c*d*f*h +  ((-1)) *a*e*f*h +  (1) *d*e*f*h +  ((-1)) *b*c*g*h +  (1) *a*d*g*h +  (1) *b*e*g*h +  ((-1)) *a*f*g*h +  ((-1)) *a*c*h^2 +  (1) *a*e*h^2 +  (1) *b*c*d*j +  (1) *a*d^2*j +  (1) *b*d*e*j +  ((-1)) *c*d*e*j +  ((-1)) *b*c*f*j +  ((-1)) *d^2*f*j +  ((-1)) *b*e*f*j +  (1) *c*e*f*j +  ((-1)) *a*f^2*j +  (1) *d*f^2*j +  ((-1)) *d*g^2*j +  (1) *f*g^2*j +  ((-1)) *b*c*h*j +  ((-1)) *a*d*h*j +  (1) *b*e*h*j +  (1) *a*f*h*j +  (1) *c*g*h*j +  ((-1)) *e*g*h*j +  ((-1)) *b*d*j^2 +  (1) *b*f*j^2 +  (1) *d*g*j^2 +  ((-1)) *f*g*j^2 +  ((-1)) *b*c^2*l +  ((-1)) *a*c*d*l +  (1) *c^2*e*l +  (1) *a*d*e*l +  (1) *b*e^2*l +  ((-1)) *c*e^2*l +  ((-1)) *a*c*f*l +  (1) *c*d*f*l +  (1) *a*e*f*l +  ((-1)) *d*e*f*l +  (1) *b*c*g*l +  (1) *a*d*g*l +  ((-1)) *b*e*g*l +  ((-1)) *a*f*g*l +  ((-1)) *d*g*h*l +  (1) *f*g*h*l +  (1) *c*h^2*l +  ((-1)) *e*h^2*l +  (1) *b*c*j*l +  ((-1)) *a*d*j*l +  ((-1)) *b*e*j*l +  (1) *a*f*j*l +  ((-1)) *c*g*j*l +  (1) *e*g*j*l +  (1) *d*h*j*l +  ((-1)) *f*h*j*l +  (1) *a*c*l^2 +  ((-1)) *a*e*l^2 +  ((-1)) *c*h*l^2 +  (1) *e*h*l^2 
F:= [
 ((-1)) *g^2 +  ((-1)) *h^2 +  (2) *g*i +  ((-2)) *i*j +  (1) *j^2 +  (2) *h*k +  ((-2)) *k*l +  (1) *l^2 ;
 ((-1)) *e^2 +  ((-1)) *f^2 +  (2) *e*i +  ((-2)) *i*j +  (1) *j^2 +  (2) *f*k +  ((-2)) *k*l +  (1) *l^2 ;
 ((-1)) *c^2 +  ((-1)) *d^2 +  (2) *c*i +  ((-2)) *i*j +  (1) *j^2 +  (2) *d*k +  ((-2)) *k*l +  (1) *l^2 ;
 (1) *a*g +  ((-1)) *b*h +  ((-1)) *a*j +  (1) *h*j +  (1) *b*l +  ((-1)) *g*l ;
 (1) *a*c +  ((-1)) *b*d +  ((-1)) *a*e +  (1) *d*e +  (1) *b*f +  ((-1)) *c*f ;
];

Certificate

CR:=[
 ((-1)) *e +  (2) *i ;  (1) *g +  ((-1)) *j ;  (1) *c +  ((-1)) *e ;  (1) *d*h +  (1) *f*h +  ((-1)) *e*j +  (2) *i*j +  ((-2)) *h*k +  ((-1)) *d*l +  ((-1)) *f*l +  (2) *k*l ;  (1) *c*e +  (1) *d*h +  ((-1)) *f*h +  ((-4)) *c*i +  (2) *e*i +  (1) *c*j +  ((-1)) *e*j +  ((-2)) *d*k +  (2) *f*k +  (1) *d*l +  ((-1)) *f*l ;  ((-1)) *f*g +  ((-1)) *b*h +  (1) *e*h +  (1) *f*j +  (1) *b*l +  ((-1)) *e*l ;  ((-1)) *a*g +  (1) *d*g +  (1) *b*h +  ((-1)) *c*h +  (1) *a*j +  ((-1)) *d*j +  ((-1)) *b*l +  (1) *c*l ;  ((-1)) *b*d +  (1) *b*f +  (1) *d*j +  ((-1)) *f*j +  ((-1)) *c*l +  (1) *e*l ; ];

C:=[
[
 ((-1)) *e +  (2) *i ;  (1) *g +  ((-1)) *j ;  (1) *c +  ((-1)) *e ;  (1) *d*h +  (1) *f*h +  ((-1)) *e*j +  (2) *i*j +  ((-2)) *h*k +  ((-1)) *d*l +  ((-1)) *f*l +  (2) *k*l ;  (1) *c*e +  (1) *d*h +  ((-1)) *f*h +  ((-4)) *c*i +  (2) *e*i +  (1) *c*j +  ((-1)) *e*j +  ((-2)) *d*k +  (2) *f*k +  (1) *d*l +  ((-1)) *f*l ;  ((-1)) *f*g +  ((-1)) *b*h +  (1) *e*h +  (1) *f*j +  (1) *b*l +  ((-1)) *e*l ;  ((-1)) *a*g +  (1) *d*g +  (1) *b*h +  ((-1)) *c*h +  (1) *a*j +  ((-1)) *d*j +  ((-1)) *b*l +  (1) *c*l ;  ((-1)) *b*d +  (1) *b*f +  (1) *d*j +  ((-1)) *f*j +  ((-1)) *c*l +  (1) *e*l ; ];

[
0; 0;  ((-1)) *g ;  (1) *c ; 0; 0; 0; ];

[
0;  (1) *c ; 0;  (1) *a ; 0; 0; ];

[
0;  (1) *g ; 0; 0;  (1) *a ; ];

];

c:=
1;