Minh
Geogebra sheet
Coq statement
Lemma minh: forall A B C D O E H I:point,
X A = 0 -> Y A = 0 -> Y O = 0 ->
equaldistance O A O B ->
equaldistance O A O C ->
equaldistance O A O D ->
orthogonal A C B D ->
collinear A C E ->
collinear B D E ->
collinear A B H ->
orthogonal E H A B ->
collinear C D I ->
middle C D I ->
collinear H E I
\/ (X B)^2 = 0 \/ X C = 0 \/ -4*X C = 0 \/ 2*X O = X C
\/ parallel A C B D.
Proof. geo_begin. tzRp (X O::X B::X C::nil). Qed.
Algebraic version
p:= ((-4)*u2^2*u3^3+8*u1*u2^2*u3^2) *e*f*k*l + (4*u2^2*u3^3+(-8)*u1*u2^2*u3^2) *d*g*k*l + ((-4)*u2^2*u3^3+8*u1*u2^2*u3^2) *d*h*k*l + (4*u2^2*u3^3+(-8)*u1*u2^2*u3^2) *f*h*k*l + (4*u2^2*u3^3+(-8)*u1*u2^2*u3^2) *e*i*k*l + ((-4)*u2^2*u3^3+8*u1*u2^2*u3^2) *g*i*k*l + (4*u2^2*u3^4+(-8)*u1*u2^2*u3^3) *e*f*j + ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *d*g*j + (4*u2^2*u3^4+(-8)*u1*u2^2*u3^3) *d*h*j + ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *f*h*j + ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *e*i*j + (4*u2^2*u3^4+(-8)*u1*u2^2*u3^3) *g*i*j + (4*u2^3*u3^3+(-8)*u1*u2^3*u3^2) *e*f*l + ((-4)*u2^3*u3^3+8*u1*u2^3*u3^2) *d*g*l + (4*u2^3*u3^3+(-8)*u1*u2^3*u3^2) *d*h*l + ((-4)*u2^3*u3^3+8*u1*u2^3*u3^2) *f*h*l + ((-4)*u2^3*u3^3+8*u1*u2^3*u3^2) *e*i*l + (4*u2^3*u3^3+(-8)*u1*u2^3*u3^2) *g*i*l + ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *e*f*m + (4*u2^2*u3^4+(-8)*u1*u2^2*u3^3) *d*g*m + ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *d*h*m + (4*u2^2*u3^4+(-8)*u1*u2^2*u3^3) *f*h*m + (4*u2^2*u3^4+(-8)*u1*u2^2*u3^3) *e*i*m + ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *g*i*m
F:= [
((-1)) *m^2 + ((-1)*u2^2+2*u1*u2) ;
((-1)) *l^2 + ((-1)*u3^2+2*u1*u3) ;
((-1)) *j^2 + ((-1)) *k^2 + (2*u1) *k ;
(2) *i + ((-1)) *k + ((-1)*u3) ;
(2) *h + ((-1)) *j + ((-1)) *l ;
(1) *j*l + ((-1)) *l*m + (u3) *k + ((-1)*u2*u3) ;
(1) *f*l + ((-1)*u3) *g ;
(1) *f*j + ((-1)) *g*k + ((-1)) *f*m + (1) *k*m + (u2) *g + ((-1)*u2) *j ;
(1) *d*m + ((-1)*u2) *e ;
(1) *e*m + ((-1)) *g*m + (u2) *d + ((-1)*u2) *f ;
(1) *i*j + ((-1)) *h*k + ((-1)) *i*l + (1) *k*l + (u3) *h + ((-1)*u3) *j ;
];
Certificate
CR:=[
((-4)*u1*u2*u3^3+8*u1^2*u2*u3^2) ; ((-1)*u2) ; (u2) ; 0; ((-4)*u2^2*u3) *d + (2*u1*u2^3+(-4)*u1^2*u2^2+(2*u2^3+2*u1*u2^2)*u3) ; ((-8)*u1*u2^2*u3) *d + (4*u2^3*u3^2) ; 0; (2*u2^2*u3^2+(-4)*u1*u2^2*u3) *e + ((-2)*u2^2*u3^2+4*u1*u2^2*u3) *g ; (4*u2^2*u3^2+(-8)*u1*u2^2*u3) *d*g + (2*u2^2*u3^2+(-4)*u1*u2^2*u3) *e*k + ((-2)*u2^2*u3^2+4*u1*u2^2*u3) *g*k + (2*u2^2*u3^3+(-4)*u2^3*u3^2+(8*u1*u2^3+(-8)*u1^2*u2^2)*u3) *e + ((-2)*u2^2*u3^3+2*u2^3*u3^2+((-4)*u1*u2^3+8*u1^2*u2^2)*u3) *g ; 0; (2*u2^2*u3^4+(-8)*u1*u2^2*u3^3+8*u1^2*u2^2*u3^2) ; 0; ((-2)*u2^3*u3^4+(12*u1*u2^3+(-8)*u1^2*u2^2)*u3^3+((-16)*u1^2*u2^3+16*u1^3*u2^2)*u3^2) ; (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *k*l + ((-2)*u2^2*u3^4+12*u1*u2^2*u3^3+(-16)*u1^2*u2^2*u3^2) *j + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *l ; ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *e + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *m ; (4*u2^2*u3^3+(-8)*u1*u2^2*u3^2) *e*k + ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *k*m + ((-4)*u2^3*u3^3+8*u1*u2^3*u3^2) *e + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *m ; (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *d*k + ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *f*k + ((-2)*u2^2*u3^4+(2*u2^3+4*u1*u2^2)*u3^3+(-4)*u1*u2^3*u3^2) *d + (2*u2^2*u3^4+(2*u2^3+(-4)*u1*u2^2)*u3^3+(-4)*u1*u2^3*u3^2) *f ; (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *d*k*l + ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *f*k*l + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *d*j + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *f*j + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *d*l + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *f*l + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *d*m + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *f*m ; ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *e*k*l + (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *g*k*l + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *e*j + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *g*j + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *e*l + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *g*l + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *e*m + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *g*m ; (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *d + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *f ; ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *d*k + (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *f*k + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *d + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *f ; ((-4)*u2^2*u3^4+16*u1*u2^2*u3^3+(-16)*u1^2*u2^2*u3^2) *d + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *f + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *k ; ];
C:=[
[
((-4)*u1*u2*u3^3+8*u1^2*u2*u3^2) ; ((-1)*u2) ; (u2) ; 0; ((-4)*u2^2*u3) *d + (2*u1*u2^3+(-4)*u1^2*u2^2+(2*u2^3+2*u1*u2^2)*u3) ; ((-8)*u1*u2^2*u3) *d + (4*u2^3*u3^2) ; 0; (2*u2^2*u3^2+(-4)*u1*u2^2*u3) *e + ((-2)*u2^2*u3^2+4*u1*u2^2*u3) *g ; (4*u2^2*u3^2+(-8)*u1*u2^2*u3) *d*g + (2*u2^2*u3^2+(-4)*u1*u2^2*u3) *e*k + ((-2)*u2^2*u3^2+4*u1*u2^2*u3) *g*k + (2*u2^2*u3^3+(-4)*u2^3*u3^2+(8*u1*u2^3+(-8)*u1^2*u2^2)*u3) *e + ((-2)*u2^2*u3^3+2*u2^3*u3^2+((-4)*u1*u2^3+8*u1^2*u2^2)*u3) *g ; 0; (2*u2^2*u3^4+(-8)*u1*u2^2*u3^3+8*u1^2*u2^2*u3^2) ; 0; ((-2)*u2^3*u3^4+(12*u1*u2^3+(-8)*u1^2*u2^2)*u3^3+((-16)*u1^2*u2^3+16*u1^3*u2^2)*u3^2) ; (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *k*l + ((-2)*u2^2*u3^4+12*u1*u2^2*u3^3+(-16)*u1^2*u2^2*u3^2) *j + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *l ; ((-4)*u2^2*u3^4+8*u1*u2^2*u3^3) *e + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *m ; (4*u2^2*u3^3+(-8)*u1*u2^2*u3^2) *e*k + ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *k*m + ((-4)*u2^3*u3^3+8*u1*u2^3*u3^2) *e + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *m ; (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *d*k + ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *f*k + ((-2)*u2^2*u3^4+(2*u2^3+4*u1*u2^2)*u3^3+(-4)*u1*u2^3*u3^2) *d + (2*u2^2*u3^4+(2*u2^3+(-4)*u1*u2^2)*u3^3+(-4)*u1*u2^3*u3^2) *f ; (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *d*k*l + ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *f*k*l + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *d*j + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *f*j + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *d*l + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *f*l + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *d*m + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *f*m ; ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *e*k*l + (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *g*k*l + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *e*j + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *g*j + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *e*l + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *g*l + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *e*m + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *g*m ; (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *d + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *f ; ((-2)*u2^2*u3^3+4*u1*u2^2*u3^2) *d*k + (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *f*k + (2*u2^3*u3^3+(-4)*u1*u2^3*u3^2) *d + ((-2)*u2^3*u3^3+4*u1*u2^3*u3^2) *f ; ((-4)*u2^2*u3^4+16*u1*u2^2*u3^3+(-16)*u1^2*u2^2*u3^2) *d + (2*u2^2*u3^4+(-4)*u1*u2^2*u3^3) *f + ((-2)*u2^2*u3^4+4*u1*u2^2*u3^3) *k ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; (1) *j ; (1) *k ; 0; 0; 0; ((-1)*u2) *m ; 0; 0; 0; 0; 0; 0; (u2) *f + ((-1)*u2) *k ; ];
[
(1) ; ((-2)*u2) *g ; ((-2)*u2*u3) *f + (2*u1*u2^2+(-4)*u1^2*u2+2*u1*u2*u3) ; ((-4)*u1*u2*u3) *f + (2*u2^2*u3^2) ; 0; 0; 0; 0; ((-4)*u1*u3^3+8*u1^2*u3^2) *k ; 0; 0; 0; ((-4)*u1*u2*u3^3+8*u1^2*u2*u3^2) *g + ((-2)*u2*u3^4+8*u1*u2*u3^3+(-8)*u1^2*u2*u3^2) *m ; 0; (2*u2^2*u3^3+(-4)*u1*u2^2*u3^2) *f ; 0; 0; 0; 0; ((-2)*u2*u3^4+8*u1*u2*u3^3+(-8)*u1^2*u2*u3^2) *k ; ];
[
0; (2*u1*u2) *k ; (((-4)*u1*u2^2+4*u1^2*u2)*u3) ; (2*u1*u2*u3) ; (u2*u3^2+(-4)*u1*u2*u3) *m ; (((-2)*u1*u2^2+4*u1^2*u2)*u3) *g + (((-1)*u2^2+2*u1*u2)*u3^2+(4*u1*u2^2+(-8)*u1^2*u2)*u3) *m ; 0; (4*u1*u3^3+(-8)*u1^2*u3^2) *k ; 0; 0; 0; (4*u1^2*u2*u3^2) *m ; 0; ((-2)*u1*u2^2*u3^2) *k ; 0; 0; ((-4)*u1^2*u2^2*u3^2) ; 0; ((-4)*u1^2*u2*u3^2) *f + (2*u2*u3^4+(-8)*u1*u2*u3^3+8*u1^2*u2*u3^2) *k ; ];
[
(1) *l ; 0; 0; 0; (2*u1*u3) *f ; 0; 0; 0; 0; 0; ((-2)*u1*u3^3+4*u1^2*u3^2) ; 0; (u3^3+(-2)*u1*u3^2) *m ; 0; 0; 0; (u2*u3^2) *j + ((-1)*u2*u3^2) *m ; 0; ];
[
((-2)*u1) ; 0; 0; ((-2)*u1+u3) *g + (2*u1+(-1)*u3) *m ; 0; 0; 0; 0; 0; ((-1)*u3^2+2*u1*u3) *l ; (u3^2+(-2)*u1*u3) *j + ((-1)*u3^2+2*u1*u3) *m ; 0; 0; 0; 0; 0; 0; ];
[
0; 0; ((-1)) *g + (1) *m ; 0; 0; 0; 0; 0; (u3) *l ; 0; ((-1)*u3) *f ; 0; 0; 0; 0; 0; ];
[
(1) *g ; 0; 0; 0; 0; 0; 0; (2*u1*u3) *j ; 0; 0; 0; 0; (2*u1*u3) *f ; 0; 0; ];
[
((-1)) *k ; 0; 0; 0; 0; 0; 0; 0; (u3) *j + (u3) *m ; 0; 0; (u3) *l ; 0; ((-1)*u3) *l ; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) *l ; 0; 0; 0; ((-1)) *j + (1) *m ; 0; ];
[
0; 0; ((-1)) *m ; (u2) ; 0; 0; 0; 0; 0; 0; 0; ((-1)) *e + (1) *g ; ];
[
0; (u2) ; (1) *m ; 0; 0; 0; 0; 0; 0; 0; (1) *d ; ];
];
c:=
(-1);