Bisectors
Geogebra sheet
Coq statement
Lemma bissectrices: forall A B C M:point,
equaltangente C A M M A B ->
equaltangente A B M M B C ->
equaltangente B C M M C A
\/ equal3 A B.
Proof. geo_begin. tzR. Qed.
Algebraic version
p:= (1) *a^2*b*c^2*d + (1) *b^3*c^2*d + ((-2)) *a^3*c*d^2 + ((-2)) *a*b^2*c*d^2 + ((-1)) *a^2*b*d^3 + ((-1)) *b^3*d^3 + (2) *a^2*c*d^3 + (2) *b^2*c*d^3 + ((-1)) *a^2*b*c^2*e + ((-1)) *b^3*c^2*e + (2) *a^3*c*d*e + (2) *a*b^2*c*d*e + ((-2)) *a*b*c^2*d*e + (1) *a^2*b*d^2*e + (1) *b^3*d^2*e + (2) *a^2*c*d^2*e + ((-2)) *b^2*c*d^2*e + (2) *a*b*d^3*e + ((-4)) *a*c*d^3*e + (2) *a*b*c^2*e^2 + ((-4)) *a^2*c*d*e^2 + (1) *b*c^2*d*e^2 + ((-2)) *a*b*d^2*e^2 + (2) *a*c*d^2*e^2 + ((-1)) *b*d^3*e^2 + (2) *c*d^3*e^2 + ((-1)) *b*c^2*e^3 + (2) *a*c*d*e^3 + (1) *b*d^2*e^3 + ((-2)) *c*d^2*e^3 + (2) *a^3*c*d*f + (2) *a*b^2*c*d*f + (2) *a^2*b*d^2*f + (2) *b^3*d^2*f + ((-2)) *a^2*c*d^2*f + ((-2)) *b^2*c*d^2*f + ((-2)) *a^3*c*e*f + ((-2)) *a*b^2*c*e*f + ((-2)) *a^2*b*d*e*f + ((-2)) *b^3*d*e*f + ((-2)) *a^2*c*d*e*f + (2) *b^2*c*d*e*f + ((-4)) *a*b*d^2*e*f + (4) *a*c*d^2*e*f + (4) *a^2*c*e^2*f + (4) *a*b*d*e^2*f + ((-2)) *a*c*d*e^2*f + (2) *b*d^2*e^2*f + ((-2)) *c*d^2*e^2*f + ((-2)) *a*c*e^3*f + ((-2)) *b*d*e^3*f + (2) *c*d*e^3*f + ((-1)) *a^2*b*d*f^2 + ((-1)) *b^3*d*f^2 + (1) *a^2*b*e*f^2 + (1) *b^3*e*f^2 + (2) *a*b*d*e*f^2 + ((-2)) *a*b*e^2*f^2 + ((-1)) *b*d*e^2*f^2 + (1) *b*e^3*f^2 + ((-1)) *a^3*c^2*g + ((-1)) *a*b^2*c^2*g + ((-2)) *a^2*b*c*d*g + ((-2)) *b^3*c*d*g + (1) *a^2*c^2*d*g + ((-1)) *b^2*c^2*d*g + (1) *a^3*d^2*g + (1) *a*b^2*d^2*g + (4) *a*b*c*d^2*g + ((-1)) *a^2*d^3*g + (1) *b^2*d^3*g + ((-4)) *b*c*d^3*g + (2) *a^2*c^2*e*g + (2) *b^2*c^2*e*g + ((-2)) *a*c^2*d*e*g + ((-2)) *a^2*d^2*e*g + ((-2)) *b^2*d^2*e*g + (4) *b*c*d^2*e*g + (2) *a*d^3*e*g + ((-1)) *a*c^2*e^2*g + ((-2)) *b*c*d*e^2*g + (1) *c^2*d*e^2*g + (1) *a*d^2*e^2*g + ((-1)) *d^3*e^2*g + (2) *a^2*b*c*f*g + (2) *b^3*c*f*g + ((-2)) *a^3*d*f*g + ((-2)) *a*b^2*d*f*g + ((-4)) *a*b*c*d*f*g + (2) *a^2*d^2*f*g + ((-2)) *b^2*d^2*f*g + (4) *b*c*d^2*f*g + (4) *a^2*d*e*f*g + (4) *b^2*d*e*f*g + ((-4)) *b*c*d*e*f*g + ((-4)) *a*d^2*e*f*g + (2) *b*c*e^2*f*g + ((-2)) *a*d*e^2*f*g + (2) *d^2*e^2*f*g + (1) *a^3*f^2*g + (1) *a*b^2*f^2*g + ((-1)) *a^2*d*f^2*g + (1) *b^2*d*f^2*g + ((-2)) *a^2*e*f^2*g + ((-2)) *b^2*e*f^2*g + (2) *a*d*e*f^2*g + (1) *a*e^2*f^2*g + ((-1)) *d*e^2*f^2*g + (2) *a*b*c^2*g^2 + (4) *b^2*c*d*g^2 + ((-1)) *b*c^2*d*g^2 + ((-2)) *a*b*d^2*g^2 + ((-2)) *a*c*d^2*g^2 + (1) *b*d^3*g^2 + (2) *c*d^3*g^2 + ((-1)) *b*c^2*e*g^2 + (2) *a*c*d*e*g^2 + (1) *b*d^2*e*g^2 + ((-2)) *c*d^2*e*g^2 + ((-4)) *b^2*c*f*g^2 + (4) *a*b*d*f*g^2 + (2) *a*c*d*f*g^2 + ((-2)) *b*d^2*f*g^2 + ((-2)) *c*d^2*f*g^2 + ((-2)) *a*c*e*f*g^2 + ((-2)) *b*d*e*f*g^2 + (2) *c*d*e*f*g^2 + ((-2)) *a*b*f^2*g^2 + (1) *b*d*f^2*g^2 + (1) *b*e*f^2*g^2 + ((-1)) *a*c^2*g^3 + ((-2)) *b*c*d*g^3 + (1) *c^2*d*g^3 + (1) *a*d^2*g^3 + ((-1)) *d^3*g^3 + (2) *b*c*f*g^3 + ((-2)) *a*d*f*g^3 + (2) *d^2*f*g^3 + (1) *a*f^2*g^3 + ((-1)) *d*f^2*g^3 + (1) *a^3*c^2*h + (1) *a*b^2*c^2*h + ((-2)) *a^2*c^2*d*h + ((-2)) *b^2*c^2*d*h + (1) *a^3*d^2*h + (1) *a*b^2*d^2*h + (2) *a^2*b*c*e*h + (2) *b^3*c*e*h + ((-1)) *a^2*c^2*e*h + (1) *b^2*c^2*e*h + ((-2)) *a^3*d*e*h + ((-2)) *a*b^2*d*e*h + (4) *a*c^2*d*e*h + ((-1)) *a^2*d^2*e*h + (1) *b^2*d^2*e*h + ((-4)) *a*b*c*e^2*h + ((-1)) *a*c^2*e^2*h + (4) *a^2*d*e^2*h + ((-2)) *c^2*d*e^2*h + ((-1)) *a*d^2*e^2*h + (2) *b*c*e^3*h + (1) *c^2*e^3*h + ((-2)) *a*d*e^3*h + (1) *d^2*e^3*h + ((-2)) *a^2*b*c*f*h + ((-2)) *b^3*c*f*h + ((-2)) *a^2*d^2*f*h + ((-2)) *b^2*d^2*f*h + (2) *a^3*e*f*h + (2) *a*b^2*e*f*h + (4) *a*b*c*e*f*h + (4) *a*d^2*e*f*h + ((-4)) *a^2*e^2*f*h + ((-2)) *b*c*e^2*f*h + ((-2)) *d^2*e^2*f*h + (2) *a*e^3*f*h + ((-1)) *a^3*f^2*h + ((-1)) *a*b^2*f^2*h + (2) *a^2*d*f^2*h + (2) *b^2*d*f^2*h + (1) *a^2*e*f^2*h + ((-1)) *b^2*e*f^2*h + ((-4)) *a*d*e*f^2*h + (1) *a*e^2*f^2*h + (2) *d*e^2*f^2*h + ((-1)) *e^3*f^2*h + (2) *a^3*c*g*h + (2) *a*b^2*c*g*h + ((-2)) *a*b*c^2*g*h + (2) *a^2*b*d*g*h + (2) *b^3*d*g*h + (4) *b*c^2*d*g*h + ((-2)) *a*b*d^2*g*h + ((-4)) *a^2*c*e*g*h + ((-4)) *b^2*c*e*g*h + ((-2)) *b*c^2*e*g*h + ((-2)) *b*d^2*e*g*h + (2) *a*c*e^2*g*h + (2) *b*d*e^2*g*h + ((-2)) *a^2*b*f*g*h + ((-2)) *b^3*f*g*h + ((-2)) *a^2*c*f*g*h + (2) *b^2*c*f*g*h + (4) *b*d^2*f*g*h + (4) *a*c*e*f*g*h + ((-2)) *b*e^2*f*g*h + ((-2)) *c*e^2*f*g*h + (2) *a*b*f^2*g*h + ((-4)) *b*d*f^2*g*h + (2) *b*e*f^2*g*h + ((-4)) *a*b*c*g^2*h + (1) *a*c^2*g^2*h + ((-4)) *b^2*d*g^2*h + ((-2)) *c^2*d*g^2*h + (1) *a*d^2*g^2*h + (2) *b*c*e*g^2*h + (1) *c^2*e*g^2*h + ((-2)) *a*d*e*g^2*h + (1) *d^2*e*g^2*h + (4) *b^2*f*g^2*h + (2) *b*c*f*g^2*h + ((-2)) *d^2*f*g^2*h + (2) *a*e*f*g^2*h + ((-1)) *a*f^2*g^2*h + (2) *d*f^2*g^2*h + ((-1)) *e*f^2*g^2*h + (2) *a*c*g^3*h + (2) *b*d*g^3*h + ((-2)) *b*f*g^3*h + ((-2)) *c*f*g^3*h + ((-2)) *a^3*c*h^2 + ((-2)) *a*b^2*c*h^2 + ((-1)) *a^2*b*d*h^2 + ((-1)) *b^3*d*h^2 + (2) *a^2*c*d*h^2 + (2) *b^2*c*d*h^2 + ((-1)) *a^2*b*e*h^2 + ((-1)) *b^3*e*h^2 + (2) *a^2*c*e*h^2 + ((-2)) *b^2*c*e*h^2 + (2) *a*b*d*e*h^2 + ((-4)) *a*c*d*e*h^2 + (2) *a*b*e^2*h^2 + (2) *a*c*e^2*h^2 + ((-1)) *b*d*e^2*h^2 + (2) *c*d*e^2*h^2 + ((-1)) *b*e^3*h^2 + ((-2)) *c*e^3*h^2 + (2) *a^2*b*f*h^2 + (2) *b^3*f*h^2 + (2) *a^2*c*f*h^2 + (2) *b^2*c*f*h^2 + ((-4)) *a*b*e*f*h^2 + ((-4)) *a*c*e*f*h^2 + (2) *b*e^2*f*h^2 + (2) *c*e^2*f*h^2 + ((-1)) *a^3*g*h^2 + ((-1)) *a*b^2*g*h^2 + (4) *a*b*c*g*h^2 + ((-1)) *a^2*d*g*h^2 + (1) *b^2*d*g*h^2 + ((-4)) *b*c*d*g*h^2 + (2) *a^2*e*g*h^2 + (2) *b^2*e*g*h^2 + (4) *b*c*e*g*h^2 + (2) *a*d*e*g*h^2 + ((-1)) *a*e^2*g*h^2 + ((-1)) *d*e^2*g*h^2 + (2) *a^2*f*g*h^2 + ((-2)) *b^2*f*g*h^2 + ((-4)) *b*c*f*g*h^2 + ((-4)) *a*e*f*g*h^2 + (2) *e^2*f*g*h^2 + (2) *a*b*g^2*h^2 + ((-2)) *a*c*g^2*h^2 + (1) *b*d*g^2*h^2 + (2) *c*d*g^2*h^2 + ((-1)) *b*e*g^2*h^2 + ((-2)) *c*e*g^2*h^2 + ((-2)) *b*f*g^2*h^2 + (2) *c*f*g^2*h^2 + ((-1)) *a*g^3*h^2 + ((-1)) *d*g^3*h^2 + (2) *f*g^3*h^2 + (1) *a^3*h^3 + (1) *a*b^2*h^3 + ((-1)) *a^2*e*h^3 + (1) *b^2*e*h^3 + ((-1)) *a*e^2*h^3 + (1) *e^3*h^3 + ((-2)) *a^2*f*h^3 + ((-2)) *b^2*f*h^3 + (4) *a*e*f*h^3 + ((-2)) *e^2*f*h^3 + ((-2)) *a*b*g*h^3 + ((-2)) *b*e*g*h^3 + (4) *b*f*g*h^3 + (1) *a*g^2*h^3 + (1) *e*g^2*h^3 + ((-2)) *f*g^2*h^3
F:= [
((-1)) *b*c^2*d + (1) *b*c^2*e + (2) *a*c*d*e + ((-2)) *a*c*e^2 + (1) *b*d*e^2 + ((-2)) *c*d*e^2 + ((-1)) *b*e^3 + (2) *c*e^3 + ((-2)) *a*c*d*f + (2) *a*c*e*f + ((-2)) *b*d*e*f + (2) *c*d*e*f + (2) *b*e^2*f + ((-2)) *c*e^2*f + (1) *b*d*f^2 + ((-1)) *b*e*f^2 + (1) *a*c^2*g + (2) *b*c*d*g + (1) *c^2*d*g + ((-2)) *c^2*e*g + ((-2)) *a*d*e*g + (1) *a*e^2*g + (1) *d*e^2*g + ((-2)) *b*c*f*g + (2) *a*d*f*g + ((-2)) *e^2*f*g + ((-1)) *a*f^2*g + ((-1)) *d*f^2*g + (2) *e*f^2*g + ((-2)) *a*c*g^2 + ((-1)) *b*d*g^2 + ((-2)) *c*d*g^2 + ((-1)) *b*e*g^2 + (2) *c*e*g^2 + (2) *b*f*g^2 + (2) *c*f*g^2 + (1) *a*g^3 + (1) *d*g^3 + ((-2)) *f*g^3 + ((-1)) *a*c^2*h + ((-2)) *b*c*e*h + (1) *c^2*e*h + (1) *a*e^2*h + ((-1)) *e^3*h + (2) *b*c*f*h + ((-2)) *a*e*f*h + (2) *e^2*f*h + (1) *a*f^2*h + ((-1)) *e*f^2*h + (2) *a*c*g*h + (2) *b*e*g*h + ((-2)) *b*f*g*h + ((-2)) *c*f*g*h + ((-1)) *a*g^2*h + ((-1)) *e*g^2*h + (2) *f*g^2*h ;
(2) *a^3*c + (2) *a*b^2*c + ((-2)) *a*b*c^2 + (1) *a^2*b*d + (1) *b^3*d + ((-2)) *a^2*c*d + ((-2)) *b^2*c*d + (1) *b*c^2*d + (1) *a^2*b*e + (1) *b^3*e + ((-2)) *a^2*c*e + ((-2)) *b^2*c*e + (1) *b*c^2*e + ((-2)) *a*b*d*e + (2) *a*c*d*e + ((-2)) *a^2*b*f + ((-2)) *b^3*f + ((-2)) *a^2*c*f + (2) *b^2*c*f + (2) *a*c*d*f + (2) *a*c*e*f + (2) *b*d*e*f + ((-2)) *c*d*e*f + (2) *a*b*f^2 + ((-1)) *b*d*f^2 + ((-1)) *b*e*f^2 + ((-1)) *a^3*g + ((-1)) *a*b^2*g + (1) *a*c^2*g + (1) *a^2*d*g + ((-1)) *b^2*d*g + (2) *b*c*d*g + ((-1)) *c^2*d*g + (2) *a^2*f*g + (2) *b^2*f*g + ((-2)) *b*c*f*g + ((-2)) *a*d*f*g + ((-1)) *a*f^2*g + (1) *d*f^2*g + ((-1)) *a^3*h + ((-1)) *a*b^2*h + (1) *a*c^2*h + (1) *a^2*e*h + ((-1)) *b^2*e*h + (2) *b*c*e*h + ((-1)) *c^2*e*h + (2) *a^2*f*h + (2) *b^2*f*h + ((-2)) *b*c*f*h + ((-2)) *a*e*f*h + ((-1)) *a*f^2*h + (1) *e*f^2*h + (2) *a*b*g*h + ((-2)) *a*c*g*h + ((-2)) *b*f*g*h + (2) *c*f*g*h ;
];
Certificate
CR:=[
((-1)) *d^2 + (2) *d*e + ((-1)) *e^2 + ((-1)) *g^2 + (2) *g*h + ((-1)) *h^2 ; ((-1)) *a^2 + ((-1)) *b^2 + (2) *a*d + ((-1)) *d^2 + (2) *b*h + ((-1)) *h^2 ; ];
C:=[
[
((-1)) *d^2 + (2) *d*e + ((-1)) *e^2 + ((-1)) *g^2 + (2) *g*h + ((-1)) *h^2 ; ((-1)) *a^2 + ((-1)) *b^2 + (2) *a*d + ((-1)) *d^2 + (2) *b*h + ((-1)) *h^2 ; ];
];
c:=
1;