proposition: Lemma existence_projete_orthogonal : forall A B C : PO, A <> B -> exists H : PO, H = projete_orthogonal A B C.
proof: Proof. intros A B C H0; try assumption. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := / scalaire (vec A B) (vec A B) * scalaire (vec A B) (vec A C)); intros H H1; try clear existence_representant_mult_vecteur. exists H. apply def_projete_orthogonal; auto. apply (colineaire_alignes H1). apply def_orthogonal2. cut (scalaire (vec A B) (vec A B) <> 0); intros; auto with geo. VReplace (vec H C) (add_PP (mult_PP 1 (vec A C)) (mult_PP (-1) (vec A H))). rewrite H1. FVReplace (mult_PP (-1) (mult_PP (/ scalaire (vec A B) (vec A B) * scalaire (vec A B) (vec A C)) (vec A B))) (mult_PP (- (/ scalaire (vec A B) (vec A B) * scalaire (vec A B) (vec A C))) (vec A B)) (scalaire (vec A B) (vec A B)). Simplscal. field; auto. Qed.