proposition: Lemma orthogonal_non_alignes : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> orthogonal (vec A B) (vec A C) -> ~ alignes A B C.
proof: Proof. intros. cut (~ ~ orthogonal (vec A B) (vec A C)); intros. contrapose H2. apply alignes_non_orthogonal; auto. tauto. Qed.