proposition: Lemma ordre_alignement_4points : forall A B C D : PO, A <> B :>PO -> alignes A B C /\ alignes A B D -> alignes C D A /\ alignes C D B.
proof: Proof. intros. elim H0; intros H1 H2; try clear H0; try exact H2. split; [ try assumption | idtac ]. eauto with geo. eauto with geo. Qed.