proposition: Lemma alignes_paralleles : forall A B C : PO, A <> B -> A <> C -> alignes A B C -> paralleles (droite A B) (droite A C).
proof: Proof. intros. apply paralleles_sym; auto. halignes H1 x. apply colineaires_paralleles with x; intros; auto. Qed.