Bisections

Coq statement

Lemma bisections: forall A B C A1 B1 C1 H:point,
  middle B C A1 ->  orthogonal H A1 B C ->
  middle A C B1 -> orthogonal H B1 A C -> 
  middle A B C1 -> 
  orthogonal H C1 A B 
  \/ collinear A B C.
Proof. geo_begin. tzR. Qed.

Algebraic version

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

Certificate

CR:=[
 (2) *m +  ((-2)) *n ;  ((-4)) *h*j +  (4) *h*k +  (2) *j*m +  ((-4)) *k*m +  (2) *j*n ;  (4) *j*m +  ((-4)) *j*n ; 0; 0;  ((-4)) *h*j*k +  (4) *h*k^2 +  (4) *f*k*m +  ((-4)) *k^2*m +  ((-4)) *f*k*n +  (4) *j*k*n ;  ((-4)) *h*j*n +  (4) *h*k*n +  (4) *f*m*n +  ((-4)) *k*m*n +  ((-4)) *f*n^2 +  (4) *j*n^2 ;  (4) *h*j*k +  ((-4)) *h*k^2 +  (4) *a*j*m +  (4) *f*j*m +  ((-4)) *c*k*m +  ((-4)) *j*k*m +  (8) *k^2*m +  ((-4)) *a*j*n +  ((-4)) *f*j*n +  (4) *c*k*n +  ((-4)) *k^2*n +  ((-4)) *d*m*n +  (4) *h*m*n +  ((-4)) *m^2*n +  (4) *d*n^2 +  ((-4)) *h*n^2 +  (8) *m*n^2 +  ((-4)) *n^3 ;  ((-4)) *a*j^2 +  (8) *a*j*k +  (4) *j^2*k +  ((-4)) *a*k^2 +  ((-8)) *j*k^2 +  (4) *k^3 +  ((-4)) *b*j*m +  (4) *b*k*m +  (4) *b*j*n +  (4) *h*j*n +  ((-4)) *b*k*n +  ((-4)) *h*k*n +  ((-4)) *f*m*n +  (4) *j*m*n +  (4) *f*n^2 +  ((-8)) *j*n^2 +  (4) *k*n^2 ;  ((-1)) *a*g*i +  (3) *a*g*j +  ((-2)) *a*g*k +  (1) *g*i*k +  ((-3)) *g*j*k +  (4) *h*j*k +  (2) *g*k^2 +  ((-4)) *h*k^2 +  ((-2)) *a*e*m +  (2) *b*g*m +  (1) *a*i*m +  ((-1)) *a*j*m +  (2) *a*k*m +  (2) *e*k*m +  ((-4)) *f*k*m +  ((-1)) *i*k*m +  (1) *j*k*m +  (2) *k^2*m +  ((-2)) *b*m^2 +  (2) *a*e*n +  ((-2)) *b*g*n +  ((-2)) *a*j*n +  ((-2)) *e*k*n +  (4) *f*k*n +  ((-2)) *j*k*n +  (2) *b*m*n +  ((-2)) *g*m*n +  (2) *m^2*n +  (2) *g*n^2 +  ((-2)) *m*n^2 ;  (1) *a*e*i +  ((-1)) *b*g*i +  ((-1)) *a*e*j +  (1) *b*g*j +  ((-4)) *b*h*j +  (4) *d*h*j +  ((-4)) *h^2*j +  ((-1)) *a*i*j +  (1) *a*j^2 +  (4) *b*h*k +  ((-4)) *d*h*k +  (4) *h^2*k +  ((-1)) *e*i*k +  (1) *e*j*k +  (1) *i*j*k +  ((-1)) *j^2*k +  (1) *b*e*l +  ((-1)) *b*j*l +  ((-1)) *b*e*m +  ((-2)) *d*e*m +  (2) *e*h*m +  (1) *b*i*m +  (4) *b*j*m +  ((-2)) *d*j*m +  (2) *h*j*m +  ((-4)) *b*k*m +  (4) *d*k*m +  ((-4)) *h*k*m +  (2) *d*e*n +  ((-2)) *e*h*n +  (1) *g*i*n +  ((-2)) *d*j*n +  ((-1)) *g*j*n +  (6) *h*j*n +  ((-4)) *h*k*n +  ((-1)) *e*l*n +  (1) *j*l*n +  (3) *e*m*n +  ((-4)) *f*m*n +  ((-1)) *i*m*n +  ((-2)) *j*m*n +  (4) *k*m*n +  ((-2)) *e*n^2 +  (4) *f*n^2 +  ((-2)) *j*n^2 ; ];

C:=[
[
 (2) *m +  ((-2)) *n ;  ((-4)) *h*j +  (4) *h*k +  (2) *j*m +  ((-4)) *k*m +  (2) *j*n ;  (4) *j*m +  ((-4)) *j*n ; 0; 0;  ((-4)) *h*j*k +  (4) *h*k^2 +  (4) *f*k*m +  ((-4)) *k^2*m +  ((-4)) *f*k*n +  (4) *j*k*n ;  ((-4)) *h*j*n +  (4) *h*k*n +  (4) *f*m*n +  ((-4)) *k*m*n +  ((-4)) *f*n^2 +  (4) *j*n^2 ;  (4) *h*j*k +  ((-4)) *h*k^2 +  (4) *a*j*m +  (4) *f*j*m +  ((-4)) *c*k*m +  ((-4)) *j*k*m +  (8) *k^2*m +  ((-4)) *a*j*n +  ((-4)) *f*j*n +  (4) *c*k*n +  ((-4)) *k^2*n +  ((-4)) *d*m*n +  (4) *h*m*n +  ((-4)) *m^2*n +  (4) *d*n^2 +  ((-4)) *h*n^2 +  (8) *m*n^2 +  ((-4)) *n^3 ;  ((-4)) *a*j^2 +  (8) *a*j*k +  (4) *j^2*k +  ((-4)) *a*k^2 +  ((-8)) *j*k^2 +  (4) *k^3 +  ((-4)) *b*j*m +  (4) *b*k*m +  (4) *b*j*n +  (4) *h*j*n +  ((-4)) *b*k*n +  ((-4)) *h*k*n +  ((-4)) *f*m*n +  (4) *j*m*n +  (4) *f*n^2 +  ((-8)) *j*n^2 +  (4) *k*n^2 ;  ((-1)) *a*g*i +  (3) *a*g*j +  ((-2)) *a*g*k +  (1) *g*i*k +  ((-3)) *g*j*k +  (4) *h*j*k +  (2) *g*k^2 +  ((-4)) *h*k^2 +  ((-2)) *a*e*m +  (2) *b*g*m +  (1) *a*i*m +  ((-1)) *a*j*m +  (2) *a*k*m +  (2) *e*k*m +  ((-4)) *f*k*m +  ((-1)) *i*k*m +  (1) *j*k*m +  (2) *k^2*m +  ((-2)) *b*m^2 +  (2) *a*e*n +  ((-2)) *b*g*n +  ((-2)) *a*j*n +  ((-2)) *e*k*n +  (4) *f*k*n +  ((-2)) *j*k*n +  (2) *b*m*n +  ((-2)) *g*m*n +  (2) *m^2*n +  (2) *g*n^2 +  ((-2)) *m*n^2 ;  (1) *a*e*i +  ((-1)) *b*g*i +  ((-1)) *a*e*j +  (1) *b*g*j +  ((-4)) *b*h*j +  (4) *d*h*j +  ((-4)) *h^2*j +  ((-1)) *a*i*j +  (1) *a*j^2 +  (4) *b*h*k +  ((-4)) *d*h*k +  (4) *h^2*k +  ((-1)) *e*i*k +  (1) *e*j*k +  (1) *i*j*k +  ((-1)) *j^2*k +  (1) *b*e*l +  ((-1)) *b*j*l +  ((-1)) *b*e*m +  ((-2)) *d*e*m +  (2) *e*h*m +  (1) *b*i*m +  (4) *b*j*m +  ((-2)) *d*j*m +  (2) *h*j*m +  ((-4)) *b*k*m +  (4) *d*k*m +  ((-4)) *h*k*m +  (2) *d*e*n +  ((-2)) *e*h*n +  (1) *g*i*n +  ((-2)) *d*j*n +  ((-1)) *g*j*n +  (6) *h*j*n +  ((-4)) *h*k*n +  ((-1)) *e*l*n +  (1) *j*l*n +  (3) *e*m*n +  ((-4)) *f*m*n +  ((-1)) *i*m*n +  ((-2)) *j*m*n +  (4) *k*m*n +  ((-2)) *e*n^2 +  (4) *f*n^2 +  ((-2)) *j*n^2 ; ];

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

[
0;  ((-1))  ;  (1)  ;  ((-1)) *f ;  ((-1)) *h ;  (1) *c ;  (1) *d ;  (1) *a +  ((-1)) *c +  (1) *f ; 0; ];

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

];

c:=
(-1);