proposition: Lemma Exists_Intersection: forall (A B C D :PO), vecEntreDeuxVec A B C D -> exists M :PO,positifColineaire B C M /\ positifColineaire C B M /\ positifColineaire A D M.
proof: Proof. intros A B C D H. destruct (@Exists_Intersection1 A B C D) as [M [H0 H1]];auto. exists M. apply vecEntreDeuxVec_intersection_middle;auto. Qed.