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);