proposition: Lemma existence_vec_directeur : forall A B : PO, A <> B -> exists C : PO, (exists D : PO, vec_directeur (vec C D) (droite A B)).
proof: Proof. intros. exists A; exists B. apply vec_directeur_trivial; auto. Qed.