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;