proposition: Lemma orthogonal_distincts : forall A B C : PO, A <> B -> A <> C -> orthogonal (vec A B) (vec A C) -> B <> C.
proof: Proof. intros. apply non_alignes_distincts2 with A; auto. apply orthogonal_non_alignes; auto with geo. Qed.