proposition: Lemma ortho_somme : forall A B C D E F : PO, orthogonal (vec A B) (vec E F) -> orthogonal (vec C D) (vec E F) -> orthogonal (add_PP (vec A B) (vec C D)) (vec E F).
proof: Proof. intros A B C D E F H H0; try assumption. elim existence_representant_som_vecteur with (A := A) (B := B) (C := C) (D := D); intros I H1; try clear existence_representant_som_vecteur; rewrite <- H1. apply def_orthogonal2. rewrite H1. Simplscal. rewrite (def_orthogonal (A:=A) (B:=B) (C:=E) (D:=F)); auto. rewrite (def_orthogonal (A:=C) (B:=D) (C:=E) (D:=F)); auto. ring. Qed.