Pythagore

Coq statement

Lemma Pythagore: forall A B C:point,
  orthogonal A B A C ->
  distance2 A C + distance2 A B = distance2 B C.
Proof. geo_begin. tzR. Qed.

Algebraic version

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

Certificate

CR:=[
 (2)  ; ];

C:=[
[
 (2)  ; ];

];

c:=
1;