proposition: Lemma Pythagore_projete_orthogonal : forall A B C H : PO, A <> B :>PO -> H = projete_orthogonal A B C :>PO -> Rsqr (distance A C) = Rsqr (distance H A) + Rsqr (distance H C) :>R /\ Rsqr (distance B C) = Rsqr (distance H B) + Rsqr (distance H C) :>R.
proof: Proof. intros. elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H); [ intros; auto | auto | auto ]. halignes H2 k. split; [ try assumption | idtac ]. elim (Pythagore H A C); intros. apply H5. replace (vec H A) with (mult_PP (-1) (vec A H)). rewrite H4. replace (mult_PP (-1) (mult_PP k (vec A B))) with (mult_PP (- k) (vec A B)). Simplortho. Ringvec. Ringvec. elim (Pythagore H B C); intros. apply H5. replace (vec H B) with (add_PP (mult_PP 1 (vec A B)) (mult_PP (- k) (vec A B))). Simplortho. replace (mult_PP (- k) (vec A B)) with (mult_PP (-1) (mult_PP k (vec A B))). rewrite <- H4. Ringvec. Ringvec. Qed.