Threepoints
Geogebra sheet
Coq statement
Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point,
(* H1 intersection of bisections *)
middle B C A1 -> orthogonal H1 A1 B C ->
middle A C B1 -> orthogonal H1 B1 A C ->
(* H2 intersection of medians *)
collinear A A1 H2 -> collinear B B1 H2 ->
(* H3 intersection of altitudes *)
collinear B C A2 -> orthogonal A A2 B C ->
collinear A C B2 -> orthogonal B B2 A C ->
collinear A A1 H3 -> collinear B B1 H3 ->
collinear H1 H2 H3
\/ collinear A B C.
Proof. geo_begin. tzR. Qed.
Algebraic version
p:= (1) *b*g*m*o + ((-1)) *a*h*m*o + (1) *a*i*m*o + ((-1)) *g*i*m*o + ((-1)) *b*j*m*o + (1) *h*j*m*o + ((-1)) *b*g*m*p + (1) *a*h*m*p + ((-1)) *a*i*m*p + (1) *g*i*m*p + (1) *b*j*m*p + ((-1)) *h*j*m*p + ((-1)) *b*g*k*r + (1) *a*h*k*r + ((-1)) *a*i*k*r + (1) *g*i*k*r + (1) *b*j*k*r + ((-1)) *h*j*k*r + (1) *b*g*p*r + ((-1)) *a*h*p*r + (1) *a*i*p*r + ((-1)) *g*i*p*r + ((-1)) *b*j*p*r + (1) *h*j*p*r + (1) *b*g*k*s + ((-1)) *a*h*k*s + (1) *a*i*k*s + ((-1)) *g*i*k*s + ((-1)) *b*j*k*s + (1) *h*j*k*s + ((-1)) *b*g*o*s + (1) *a*h*o*s + ((-1)) *a*i*o*s + (1) *g*i*o*s + (1) *b*j*o*s + ((-1)) *h*j*o*s
F:= [
((-1)) *r + ((-1)) *s + (2) *t ;
((-1)) *o + ((-1)) *p + (2) *q ;
((-1)) *m + (2) *n + ((-1)) *r ;
((-1)) *k + (2) *l + ((-1)) *o ;
(1) *i*k + ((-1)) *k*l + (1) *j*m + ((-1)) *m*n + ((-1)) *i*o + (1) *l*o + ((-1)) *j*r + (1) *n*r ;
((-1)) *i*o + (1) *i*p + (1) *o*q + ((-1)) *p*q + ((-1)) *j*r + (1) *j*s + (1) *r*t + ((-1)) *s*t ;
(1) *g*l + ((-1)) *h*n + ((-1)) *g*p + (1) *n*p + (1) *h*s + ((-1)) *l*s ;
((-1)) *g*k + (1) *h*m + (1) *g*q + ((-1)) *m*q + ((-1)) *h*t + (1) *k*t ;
((-1)) *e*k + (1) *f*m + (1) *e*o + ((-1)) *m*o + ((-1)) *f*r + (1) *k*r ;
((-1)) *f*k + ((-1)) *e*m + (1) *f*o + (1) *k*p + ((-1)) *o*p + (1) *e*r + (1) *m*s + ((-1)) *r*s ;
(1) *c*o + ((-1)) *c*p + ((-1)) *d*r + (1) *p*r + (1) *d*s + ((-1)) *o*s ;
(1) *d*o + ((-1)) *k*o + ((-1)) *d*p + (1) *k*p + (1) *c*r + ((-1)) *m*r + ((-1)) *c*s + (1) *m*s ;
(1) *a*l + ((-1)) *b*n + ((-1)) *a*p + (1) *n*p + (1) *b*s + ((-1)) *l*s ;
((-1)) *a*k + (1) *b*m + (1) *a*q + ((-1)) *m*q + ((-1)) *b*t + (1) *k*t ;
];
Certificate
CR:=[
(6) *n + ((-6)) *s ; (12) *j + ((-8)) *n + ((-4)) *s ; ((-6)) *n + (6) *s ; ((-12)) *j + (8) *n + (4) *s ; ((-12)) *h*n + (12) *j*p + ((-8)) *n*p + (12) *n*q + (12) *h*s + ((-4)) *p*s + ((-12)) *q*s ; (12) *b*n + ((-12)) *j*p + (8) *n*p + ((-12)) *n*q + ((-12)) *b*s + (4) *p*s + (12) *q*s ; ((-18)) *a*n + (18) *g*n + (18) *a*s + ((-18)) *g*s ; 0; (36) *j*q + ((-24)) *n*q + ((-36)) *h*s + (36) *i*s + ((-12)) *q*s + (36) *h*t + ((-36)) *i*t ; 0; 0; 0; 0; 0; ((-36)) *j*q + (24) *n*q + (36) *b*s + ((-36)) *i*s + (12) *q*s + ((-36)) *b*t + (36) *i*t ; 0; 0; ((-18)) *b*g*s + (18) *a*h*s + ((-18)) *a*i*s + (18) *g*i*s + (18) *b*j*s + ((-18)) *h*j*s + (18) *b*g*t + ((-18)) *a*h*t + (18) *a*i*t + ((-18)) *g*i*t + ((-18)) *b*j*t + (18) *h*j*t + (12) *b*n*t + ((-12)) *h*n*t + ((-12)) *b*s*t + (12) *h*s*t ; (18) *b*g*p + ((-18)) *a*h*p + (18) *a*i*p + ((-18)) *g*i*p + ((-18)) *b*j*p + (18) *h*j*p + ((-18)) *b*g*q + (18) *a*h*q + ((-18)) *a*i*q + (18) *g*i*q + (18) *b*j*q + ((-18)) *h*j*q + ((-12)) *b*n*q + (12) *h*n*q + (12) *b*q*s + ((-12)) *h*q*s ; ((-9)) *b*g*m + (9) *a*h*m + ((-9)) *a*i*m + (9) *g*i*m + (9) *b*j*m + ((-9)) *h*j*m + ((-18)) *a*n*q + (18) *g*n*q + (27) *b*g*s + ((-27)) *a*h*s + (27) *a*i*s + ((-27)) *g*i*s + ((-27)) *b*j*s + (27) *h*j*s + (18) *a*q*s + ((-18)) *g*q*s + ((-18)) *b*g*t + (18) *a*h*t + ((-18)) *a*i*t + (18) *g*i*t + (18) *b*j*t + ((-18)) *h*j*t + ((-12)) *b*n*t + (12) *h*n*t + (12) *b*s*t + ((-12)) *h*s*t ; (9) *b*g*k + ((-9)) *a*h*k + (9) *a*i*k + ((-9)) *g*i*k + ((-9)) *b*j*k + (9) *h*j*k + (12) *b*j*l + ((-12)) *h*j*l + (18) *a*j*n + ((-18)) *g*j*n + ((-8)) *b*l*n + (8) *h*l*n + ((-27)) *b*g*p + (27) *a*h*p + ((-27)) *a*i*p + (27) *g*i*p + (15) *b*j*p + ((-15)) *h*j*p + (8) *b*n*p + ((-8)) *h*n*p + (18) *b*g*q + ((-18)) *a*h*q + (18) *a*i*q + ((-18)) *g*i*q + ((-18)) *b*j*q + (18) *h*j*q + ((-18)) *a*j*s + (18) *g*j*s + ((-4)) *b*l*s + (4) *h*l*s + (4) *b*p*s + ((-4)) *h*p*s ; ];
C:=[
[
(6) *n + ((-6)) *s ; (12) *j + ((-8)) *n + ((-4)) *s ; ((-6)) *n + (6) *s ; ((-12)) *j + (8) *n + (4) *s ; ((-12)) *h*n + (12) *j*p + ((-8)) *n*p + (12) *n*q + (12) *h*s + ((-4)) *p*s + ((-12)) *q*s ; (12) *b*n + ((-12)) *j*p + (8) *n*p + ((-12)) *n*q + ((-12)) *b*s + (4) *p*s + (12) *q*s ; ((-18)) *a*n + (18) *g*n + (18) *a*s + ((-18)) *g*s ; 0; (36) *j*q + ((-24)) *n*q + ((-36)) *h*s + (36) *i*s + ((-12)) *q*s + (36) *h*t + ((-36)) *i*t ; 0; 0; 0; 0; 0; ((-36)) *j*q + (24) *n*q + (36) *b*s + ((-36)) *i*s + (12) *q*s + ((-36)) *b*t + (36) *i*t ; 0; 0; ((-18)) *b*g*s + (18) *a*h*s + ((-18)) *a*i*s + (18) *g*i*s + (18) *b*j*s + ((-18)) *h*j*s + (18) *b*g*t + ((-18)) *a*h*t + (18) *a*i*t + ((-18)) *g*i*t + ((-18)) *b*j*t + (18) *h*j*t + (12) *b*n*t + ((-12)) *h*n*t + ((-12)) *b*s*t + (12) *h*s*t ; (18) *b*g*p + ((-18)) *a*h*p + (18) *a*i*p + ((-18)) *g*i*p + ((-18)) *b*j*p + (18) *h*j*p + ((-18)) *b*g*q + (18) *a*h*q + ((-18)) *a*i*q + (18) *g*i*q + (18) *b*j*q + ((-18)) *h*j*q + ((-12)) *b*n*q + (12) *h*n*q + (12) *b*q*s + ((-12)) *h*q*s ; ((-9)) *b*g*m + (9) *a*h*m + ((-9)) *a*i*m + (9) *g*i*m + (9) *b*j*m + ((-9)) *h*j*m + ((-18)) *a*n*q + (18) *g*n*q + (27) *b*g*s + ((-27)) *a*h*s + (27) *a*i*s + ((-27)) *g*i*s + ((-27)) *b*j*s + (27) *h*j*s + (18) *a*q*s + ((-18)) *g*q*s + ((-18)) *b*g*t + (18) *a*h*t + ((-18)) *a*i*t + (18) *g*i*t + (18) *b*j*t + ((-18)) *h*j*t + ((-12)) *b*n*t + (12) *h*n*t + (12) *b*s*t + ((-12)) *h*s*t ; (9) *b*g*k + ((-9)) *a*h*k + (9) *a*i*k + ((-9)) *g*i*k + ((-9)) *b*j*k + (9) *h*j*k + (12) *b*j*l + ((-12)) *h*j*l + (18) *a*j*n + ((-18)) *g*j*n + ((-8)) *b*l*n + (8) *h*l*n + ((-27)) *b*g*p + (27) *a*h*p + ((-27)) *a*i*p + (27) *g*i*p + (15) *b*j*p + ((-15)) *h*j*p + (8) *b*n*p + ((-8)) *h*n*p + (18) *b*g*q + ((-18)) *a*h*q + (18) *a*i*q + ((-18)) *g*i*q + ((-18)) *b*j*q + (18) *h*j*q + ((-18)) *a*j*s + (18) *g*j*s + ((-4)) *b*l*s + (4) *h*l*s + (4) *b*p*s + ((-4)) *h*p*s ; ];
[
0; 0; 0; 0; ((-2)) *i + (2) *q ; ((-3)) *g + (2) *n ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *i*q + ((-2)) *q^2 ; ((-3)) *g*q + (2) *n*q ; (2) *h*i + (3) *g*j + ((-2)) *j*n + ((-2)) *h*q + ((-2)) *i*q + (2) *q^2 ; ];
[
0; 0; 0; (1) *l ; 0; 0; 0; 0; 0; 0; 0; 0; (3) *p ; 0; 0; 0; 0; 0; 0; ];
[
0; ((-2)) *i + (2) *q ; 0; ((-3)) *a + (2) *n ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *i*q + ((-2)) *q^2 ; ((-3)) *a*q + (2) *n*q ; (2) *b*i + (3) *a*j + ((-2)) *j*n + ((-2)) *b*q + ((-2)) *i*q + (2) *q^2 ; ];
[
(1) *l ; 0; 0; 0; (3) *p ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; (1) ; (2) ; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *a ; (1) *b ; (1) *a ; 0; ];
[
0; 0; 0; 0; 0; 0; 0; (1) ; (2) ; 0; 0; ((-1)) *g ; (1) *h ; (1) *g ; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; (1) ; 0; 0; 0; ((-1)) *i ; 0; ];
];
c:=
9;