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