proposition: Lemma ortho_combinaison_lineaire : forall (a b : R) (A B C D E F : PO), orthogonal (vec A B) (vec E F) -> orthogonal (vec C D) (vec E F) -> orthogonal (add_PP (mult_PP a (vec A B)) (mult_PP b (vec C D))) (vec E F).
proof: Proof. intros a b A B C D E F H H0; try assumption. elim existence_representant_comb_lin_vecteur with (A := A) (B := B) (C := C) (D := D) (a := a) (b := b); intros E0 H1; try clear existence_representant_comb_lin_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.