Isoceles

Coq statement

Lemma isoceles: forall A B C:point,
  equaltangente A B C B C A ->
  distance2 A B = distance2 A C
  \/ collinear A B C.
Proof. geo_begin. tzR. Qed.

Algebraic version

p:=  (1) *a^3*b +  ((-1)) *a^3*c +  (2) *a*b^2*c +  ((-3)) *a*b*c^2 +  (1) *a*c^3 +  ((-2)) *a*b^2*d +  (2) *a*b*c*d +  (1) *a*b*d^2 +  ((-1)) *a*c*d^2 +  ((-1)) *a^2*b*e +  ((-2)) *b^2*c*e +  (1) *b*c^2*e +  (1) *a^2*d*e +  (2) *b^2*d*e +  (2) *b*c*d*e +  ((-1)) *c^2*d*e +  ((-3)) *b*d^2*e +  (1) *d^3*e +  ((-1)) *a*b*e^2 +  (1) *a*c*e^2 +  (1) *b*e^3 +  ((-1)) *d*e^3 +  ((-2)) *a^2*b*f +  (3) *a^2*c*f +  (2) *b*c^2*f +  ((-1)) *c^3*f +  ((-1)) *a^2*d*f +  ((-4)) *b*c*d*f +  (1) *c^2*d*f +  (2) *b*d^2*f +  (1) *c*d^2*f +  ((-1)) *d^3*f +  (4) *a*b*e*f +  ((-2)) *a*c*e*f +  ((-2)) *a*d*e*f +  ((-2)) *b*e^2*f +  ((-1)) *c*e^2*f +  (3) *d*e^2*f +  ((-2)) *a*c*f^2 +  (2) *a*d*f^2 +  (2) *c*e*f^2 +  ((-2)) *d*e*f^2 
F:= [
 ((-1)) *a^3*b +  (1) *a^3*c +  ((-2)) *a*b^2*c +  (3) *a*b*c^2 +  ((-1)) *a*c^3 +  (2) *a*b^2*d +  ((-2)) *a*b*c*d +  ((-1)) *a*b*d^2 +  (1) *a*c*d^2 +  (1) *a^2*b*e +  (2) *b^2*c*e +  ((-1)) *b*c^2*e +  ((-1)) *a^2*d*e +  ((-2)) *b^2*d*e +  ((-2)) *b*c*d*e +  (1) *c^2*d*e +  (3) *b*d^2*e +  ((-1)) *d^3*e +  (1) *a*b*e^2 +  ((-1)) *a*c*e^2 +  ((-1)) *b*e^3 +  (1) *d*e^3 +  (2) *a^2*b*f +  ((-3)) *a^2*c*f +  ((-2)) *b*c^2*f +  (1) *c^3*f +  (1) *a^2*d*f +  (4) *b*c*d*f +  ((-1)) *c^2*d*f +  ((-2)) *b*d^2*f +  ((-1)) *c*d^2*f +  (1) *d^3*f +  ((-4)) *a*b*e*f +  (2) *a*c*e*f +  (2) *a*d*e*f +  (2) *b*e^2*f +  (1) *c*e^2*f +  ((-3)) *d*e^2*f +  (2) *a*c*f^2 +  ((-2)) *a*d*f^2 +  ((-2)) *c*e*f^2 +  (2) *d*e*f^2 ;
];

Certificate

CR:=[
 (1)  ; ];

C:=[
[
 (1)  ; ];

];

c:=
(-1);