Medians

Geogebra sheet

Coq statement

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

Algebraic version

p:=  ((-1)) *a*e*g*i +  (1) *b*g^2*i +  (1) *a*e*g*j +  ((-1)) *b*g^2*j +  (1) *a*g*i*k +  ((-1)) *g^2*i*k +  ((-1)) *a*g*j*k +  (1) *g^2*j*k +  (1) *a*e^2*l +  ((-1)) *b*e*g*l +  ((-1)) *a*e*j*l +  (1) *b*g*j*l +  ((-1)) *a*e*k*l +  (1) *e*g*k*l +  (1) *a*j*k*l +  ((-1)) *g*j*k*l +  ((-1)) *a*e^2*m +  (1) *b*e*g*m +  (1) *a*e*i*m +  ((-1)) *b*g*i*m +  (1) *a*e*k*m +  ((-1)) *e*g*k*m +  ((-1)) *a*i*k*m +  (1) *g*i*k*m +  ((-1)) *b*g*i*n +  (1) *e*g*i*n +  (1) *b*g*j*n +  ((-1)) *e*g*j*n +  (1) *b*e*l*n +  ((-1)) *e^2*l*n +  ((-1)) *b*j*l*n +  (1) *e*j*l*n +  ((-1)) *b*e*m*n +  (1) *e^2*m*n +  (1) *b*i*m*n +  ((-1)) *e*i*m*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*c +  ((-1)) *b*d +  ((-1)) *a*j +  (1) *d*j +  (1) *b*m +  ((-1)) *c*m ;
 (1) *a*f +  ((-1)) *b*h +  ((-1)) *a*i +  (1) *h*i +  (1) *b*l +  ((-1)) *f*l ;
];

Certificate

CR:=[
 (2) *m +  ((-2)) *n ;  ((-2)) *h*j +  (2) *h*k +  ((-4)) *j*m +  ((-4)) *k*m +  (6) *j*n +  (2) *k*n ;  (8) *h*j +  ((-8)) *h*k +  ((-8)) *f*m +  (12) *j*m +  (8) *k*m +  (8) *f*n +  ((-20)) *j*n ; 0;  (6) *h*j*m +  (6) *a*k*m +  ((-6)) *h*k*m +  (6) *b*m^2 +  ((-2)) *c*m^2 +  ((-4)) *f*m^2 +  ((-2)) *j*m^2 +  (2) *k*m^2 +  ((-4)) *h*j*n +  ((-6)) *a*k*n +  (4) *h*k*n +  ((-12)) *b*m*n +  (2) *c*m*n +  (8) *f*m*n +  (2) *j*m*n +  (6) *b*n^2 +  ((-4)) *f*n^2 +  ((-2)) *j*n^2 ;  ((-2)) *h*j^2 +  (2) *h*j*k +  (2) *j^2*m +  ((-4)) *j*k*m +  (2) *j*k*n ;  ((-4)) *a*h*j +  (4) *a*h*k +  (2) *a*e*m +  (4) *a*f*m +  ((-4)) *b*h*m +  ((-6)) *h*j*m +  ((-12)) *a*k*m +  (10) *h*k*m +  ((-4)) *b*m^2 +  (2) *c*m^2 +  (4) *f*m^2 +  (2) *j*m^2 +  ((-4)) *k*m^2 +  ((-2)) *a*e*n +  ((-4)) *a*f*n +  (4) *b*h*n +  (4) *a*j*n +  (8) *h*j*n +  (8) *a*k*n +  ((-12)) *h*k*n +  (12) *b*m*n +  ((-2)) *c*m*n +  ((-2)) *e*m*n +  ((-12)) *f*m*n +  ((-2)) *j*m*n +  (6) *k*m*n +  ((-8)) *b*n^2 +  (2) *e*n^2 +  (8) *f*n^2 +  ((-2)) *j*n^2 ;  ((-2)) *a*e*j +  (2) *b*g*j +  (4) *b*h*j +  (2) *h*j^2 +  (2) *a*e*k +  ((-2)) *b*g*k +  ((-4)) *b*h*k +  (2) *a*j*k +  ((-2)) *g*j*k +  ((-6)) *h*j*k +  ((-2)) *a*k^2 +  (2) *g*k^2 +  (4) *h*k^2 +  ((-2)) *b*e*m +  ((-2)) *b*j*m +  ((-2)) *j^2*m +  (4) *b*k*m +  (2) *e*k*m +  (6) *j*k*m +  ((-4)) *k^2*m +  (2) *b*e*n +  ((-4)) *b*j*n +  (2) *e*j*n +  (2) *b*k*n +  ((-4)) *e*k*n ;  (1) *a*e*g +  ((-1)) *b*g^2 +  ((-8)) *a*h*j +  (8) *h^2*j +  ((-1)) *a*g*k +  (1) *g^2*k +  (8) *a*h*k +  ((-8)) *h^2*k +  ((-1)) *a*e*m +  (8) *a*f*m +  (1) *b*g*m +  ((-8)) *f*h*m +  ((-12)) *a*j*m +  (6) *h*j*m +  ((-13)) *a*k*m +  ((-1)) *g*k*m +  (14) *h*k*m +  ((-6)) *b*m^2 +  (2) *c*m^2 +  (4) *f*m^2 +  (2) *j*m^2 +  ((-2)) *k*m^2 +  ((-8)) *a*f*n +  (1) *b*g*n +  ((-1)) *e*g*n +  (8) *f*h*n +  (20) *a*j*n +  ((-16)) *h*j*n +  (6) *a*k*n +  ((-4)) *h*k*n +  (11) *b*m*n +  ((-2)) *c*m*n +  (1) *e*m*n +  ((-8)) *f*m*n +  ((-2)) *j*m*n +  ((-6)) *b*n^2 +  (4) *f*n^2 +  (2) *j*n^2 ;  ((-1)) *a*e^2 +  (1) *b*e*g +  (1) *a*e*j +  ((-1)) *b*g*j +  (2) *b*h*j +  ((-4)) *f*h*j +  (2) *h*j^2 +  (1) *a*e*k +  ((-1)) *e*g*k +  ((-2)) *b*h*k +  (4) *f*h*k +  ((-1)) *a*j*k +  (1) *g*j*k +  ((-2)) *h*j*k +  (6) *b*c*m +  ((-8)) *b*f*m +  ((-4)) *c*f*m +  (8) *f^2*m +  (6) *b*j*m +  ((-2)) *c*j*m +  ((-4)) *f*j*m +  ((-2)) *j^2*m +  ((-4)) *b*k*m +  (4) *j*k*m +  ((-6)) *b*c*n +  ((-1)) *b*e*n +  (1) *e^2*n +  (8) *b*f*n +  (4) *c*f*n +  ((-8)) *f^2*n +  ((-7)) *b*j*n +  (2) *c*j*n +  ((-1)) *e*j*n +  (8) *f*j*n +  (6) *b*k*n +  ((-4)) *f*k*n +  ((-2)) *j*k*n ; ];

C:=[
[
 (2) *m +  ((-2)) *n ;  ((-2)) *h*j +  (2) *h*k +  ((-4)) *j*m +  ((-4)) *k*m +  (6) *j*n +  (2) *k*n ;  (8) *h*j +  ((-8)) *h*k +  ((-8)) *f*m +  (12) *j*m +  (8) *k*m +  (8) *f*n +  ((-20)) *j*n ; 0;  (6) *h*j*m +  (6) *a*k*m +  ((-6)) *h*k*m +  (6) *b*m^2 +  ((-2)) *c*m^2 +  ((-4)) *f*m^2 +  ((-2)) *j*m^2 +  (2) *k*m^2 +  ((-4)) *h*j*n +  ((-6)) *a*k*n +  (4) *h*k*n +  ((-12)) *b*m*n +  (2) *c*m*n +  (8) *f*m*n +  (2) *j*m*n +  (6) *b*n^2 +  ((-4)) *f*n^2 +  ((-2)) *j*n^2 ;  ((-2)) *h*j^2 +  (2) *h*j*k +  (2) *j^2*m +  ((-4)) *j*k*m +  (2) *j*k*n ;  ((-4)) *a*h*j +  (4) *a*h*k +  (2) *a*e*m +  (4) *a*f*m +  ((-4)) *b*h*m +  ((-6)) *h*j*m +  ((-12)) *a*k*m +  (10) *h*k*m +  ((-4)) *b*m^2 +  (2) *c*m^2 +  (4) *f*m^2 +  (2) *j*m^2 +  ((-4)) *k*m^2 +  ((-2)) *a*e*n +  ((-4)) *a*f*n +  (4) *b*h*n +  (4) *a*j*n +  (8) *h*j*n +  (8) *a*k*n +  ((-12)) *h*k*n +  (12) *b*m*n +  ((-2)) *c*m*n +  ((-2)) *e*m*n +  ((-12)) *f*m*n +  ((-2)) *j*m*n +  (6) *k*m*n +  ((-8)) *b*n^2 +  (2) *e*n^2 +  (8) *f*n^2 +  ((-2)) *j*n^2 ;  ((-2)) *a*e*j +  (2) *b*g*j +  (4) *b*h*j +  (2) *h*j^2 +  (2) *a*e*k +  ((-2)) *b*g*k +  ((-4)) *b*h*k +  (2) *a*j*k +  ((-2)) *g*j*k +  ((-6)) *h*j*k +  ((-2)) *a*k^2 +  (2) *g*k^2 +  (4) *h*k^2 +  ((-2)) *b*e*m +  ((-2)) *b*j*m +  ((-2)) *j^2*m +  (4) *b*k*m +  (2) *e*k*m +  (6) *j*k*m +  ((-4)) *k^2*m +  (2) *b*e*n +  ((-4)) *b*j*n +  (2) *e*j*n +  (2) *b*k*n +  ((-4)) *e*k*n ;  (1) *a*e*g +  ((-1)) *b*g^2 +  ((-8)) *a*h*j +  (8) *h^2*j +  ((-1)) *a*g*k +  (1) *g^2*k +  (8) *a*h*k +  ((-8)) *h^2*k +  ((-1)) *a*e*m +  (8) *a*f*m +  (1) *b*g*m +  ((-8)) *f*h*m +  ((-12)) *a*j*m +  (6) *h*j*m +  ((-13)) *a*k*m +  ((-1)) *g*k*m +  (14) *h*k*m +  ((-6)) *b*m^2 +  (2) *c*m^2 +  (4) *f*m^2 +  (2) *j*m^2 +  ((-2)) *k*m^2 +  ((-8)) *a*f*n +  (1) *b*g*n +  ((-1)) *e*g*n +  (8) *f*h*n +  (20) *a*j*n +  ((-16)) *h*j*n +  (6) *a*k*n +  ((-4)) *h*k*n +  (11) *b*m*n +  ((-2)) *c*m*n +  (1) *e*m*n +  ((-8)) *f*m*n +  ((-2)) *j*m*n +  ((-6)) *b*n^2 +  (4) *f*n^2 +  (2) *j*n^2 ;  ((-1)) *a*e^2 +  (1) *b*e*g +  (1) *a*e*j +  ((-1)) *b*g*j +  (2) *b*h*j +  ((-4)) *f*h*j +  (2) *h*j^2 +  (1) *a*e*k +  ((-1)) *e*g*k +  ((-2)) *b*h*k +  (4) *f*h*k +  ((-1)) *a*j*k +  (1) *g*j*k +  ((-2)) *h*j*k +  (6) *b*c*m +  ((-8)) *b*f*m +  ((-4)) *c*f*m +  (8) *f^2*m +  (6) *b*j*m +  ((-2)) *c*j*m +  ((-4)) *f*j*m +  ((-2)) *j^2*m +  ((-4)) *b*k*m +  (4) *j*k*m +  ((-6)) *b*c*n +  ((-1)) *b*e*n +  (1) *e^2*n +  (8) *b*f*n +  (4) *c*f*n +  ((-8)) *f^2*n +  ((-7)) *b*j*n +  (2) *c*j*n +  ((-1)) *e*j*n +  (8) *f*j*n +  (6) *b*k*n +  ((-4)) *f*k*n +  ((-2)) *j*k*n ; ];

[
 (1) *c ; 0;  ((-6)) *j ; 0;  ((-3)) *b*j +  (1) *c*j ; 0;  (3) *b*j +  ((-1)) *c*j ; 0; 0; ];

[
 (2)  ;  ((-2))  ;  (1) *a ;  ((-1)) *b ;  ((-1)) *a ;  (1) *b ;  ((-3)) *a +  (2) *h ; 0; ];

];

c:=
1;