proposition: Lemma alignes_droite2 : forall A B C : PO, A <> B :>PO -> B <> C :>PO -> alignes A B C -> droite A B = droite B C.
proof: Proof. intros. rewrite droite_permute; auto. apply alignes_droite; auto with geo. Qed.