# Chords

Geogebra sheet

## 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;
```