proposition: Lemma existence_parallele : forall A B C : PO, A <> B -> exists D, paralleles (droite A B) (droite C D).
proof: Proof. intros. soit_milieu M A C. soit_image D M B. exists D. eapply colineaires_paralleles with (k:=-1);auto. unfold not;intro;subst C. assert (A=B). rewrite H2 in H1. eapply unicite_symetrique;eauto. auto. VReplace (mult_PP (-1) (vec C D)) (vec D C). assert (parallelogramme A B C D). assert (T:=(caract_milieu_parallelogramme A B C D)). rewrite H1 in H2. tauto. auto. Qed.