proposition: Lemma opp_orthogonal3 : forall A B C D : PO, orthogonal (vec A B) (vec C D) -> orthogonal (vec A B) (vec D C).
proof: Proof. intros. apply ortho_sym. replace (vec D C) with (mult_PP (-1) (vec C D)); [ Simplortho | Ringvec ]. Qed.