proposition: Theorem Pythagore : forall A B C : PO, orthogonal (vec A B) (vec A C) <-> Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) :>R.
proof: Proof. intros. unfold Rsqr in |- *; repeat rewrite <- carre_scalaire_distance. elim (triangle_Pythagore A B C); intros. red in |- *; split; intros. apply H; auto with geo. apply def_orthogonal2; auto. Qed.