proposition: Lemma ortho_mult : forall (a : R) (A B C D : PO), orthogonal (vec A B) (vec C D) -> orthogonal (mult_PP a (vec A B)) (vec C D).
proof: Proof. intros. replace (mult_PP a (vec A B)) with (add_PP (mult_PP a (vec A B)) (mult_PP 0 (vec A B))). apply ortho_combinaison_lineaire; auto. Ringvec. Qed.