proposition: Lemma ortho_sym : forall A B C D : PO, orthogonal (vec A B) (vec C D) -> orthogonal (vec C D) (vec A B).
proof: Proof. intros A B C D H; try assumption. apply def_orthogonal2. rewrite scalaire_sym. rewrite (def_orthogonal (A:=A) (B:=B) (C:=C) (D:=D)); auto. Qed.